module Spec.Hash.Test

open FStar.Seq

//
// Test 1
//

let test1_plaintext = [0x61uy; 0x62uy; 0x63uy]

let test1_expected224 =
  [
    0x23uy; 0x09uy; 0x7duy; 0x22uy; 0x34uy; 0x05uy; 0xd8uy; 0x22uy; 0x86uy; 0x42uy; 0xa4uy; 0x77uy;
    0xbduy; 0xa2uy; 0x55uy; 0xb3uy; 0x2auy; 0xaduy; 0xbcuy; 0xe4uy; 0xbduy; 0xa0uy; 0xb3uy; 0xf7uy;
    0xe3uy; 0x6cuy; 0x9duy; 0xa7uy
  ]

let test1_expected256 =
  [
    0xbauy; 0x78uy; 0x16uy; 0xbfuy; 0x8fuy; 0x01uy; 0xcfuy; 0xeauy; 0x41uy; 0x41uy; 0x40uy; 0xdeuy;
    0x5duy; 0xaeuy; 0x22uy; 0x23uy; 0xb0uy; 0x03uy; 0x61uy; 0xa3uy; 0x96uy; 0x17uy; 0x7auy; 0x9cuy;
    0xb4uy; 0x10uy; 0xffuy; 0x61uy; 0xf2uy; 0x00uy; 0x15uy; 0xaduy
  ]

let test1_expected384 =
  [
    0xcbuy; 0x00uy; 0x75uy; 0x3fuy; 0x45uy; 0xa3uy; 0x5euy; 0x8buy; 0xb5uy; 0xa0uy; 0x3duy; 0x69uy;
    0x9auy; 0xc6uy; 0x50uy; 0x07uy; 0x27uy; 0x2cuy; 0x32uy; 0xabuy; 0x0euy; 0xdeuy; 0xd1uy; 0x63uy;
    0x1auy; 0x8buy; 0x60uy; 0x5auy; 0x43uy; 0xffuy; 0x5buy; 0xeduy; 0x80uy; 0x86uy; 0x07uy; 0x2buy;
    0xa1uy; 0xe7uy; 0xccuy; 0x23uy; 0x58uy; 0xbauy; 0xecuy; 0xa1uy; 0x34uy; 0xc8uy; 0x25uy; 0xa7uy
  ]

let test1_expected512 =
  [
    0xdduy; 0xafuy; 0x35uy; 0xa1uy; 0x93uy; 0x61uy; 0x7auy; 0xbauy; 0xccuy; 0x41uy; 0x73uy; 0x49uy;
    0xaeuy; 0x20uy; 0x41uy; 0x31uy; 0x12uy; 0xe6uy; 0xfauy; 0x4euy; 0x89uy; 0xa9uy; 0x7euy; 0xa2uy;
    0x0auy; 0x9euy; 0xeeuy; 0xe6uy; 0x4buy; 0x55uy; 0xd3uy; 0x9auy; 0x21uy; 0x92uy; 0x99uy; 0x2auy;
    0x27uy; 0x4fuy; 0xc1uy; 0xa8uy; 0x36uy; 0xbauy; 0x3cuy; 0x23uy; 0xa3uy; 0xfeuy; 0xebuy; 0xbduy;
    0x45uy; 0x4duy; 0x44uy; 0x23uy; 0x64uy; 0x3cuy; 0xe8uy; 0x0euy; 0x2auy; 0x9auy; 0xc9uy; 0x4fuy;
    0xa5uy; 0x4cuy; 0xa4uy; 0x9fuy
  ]

//
// Test 2
//

// This empty list must have its type annotated, otherwise
// length preconditions on test vectors cannot be normalized
let test2_plaintext: list UInt8.t = []

let test2_expected224 =
  [
    0xd1uy; 0x4auy; 0x02uy; 0x8cuy; 0x2auy; 0x3auy; 0x2buy; 0xc9uy; 0x47uy; 0x61uy; 0x02uy; 0xbbuy;
    0x28uy; 0x82uy; 0x34uy; 0xc4uy; 0x15uy; 0xa2uy; 0xb0uy; 0x1fuy; 0x82uy; 0x8euy; 0xa6uy; 0x2auy;
    0xc5uy; 0xb3uy; 0xe4uy; 0x2fuy
  ]

let test2_expected256 =
  [
    0xe3uy; 0xb0uy; 0xc4uy; 0x42uy; 0x98uy; 0xfcuy; 0x1cuy; 0x14uy; 0x9auy; 0xfbuy; 0xf4uy; 0xc8uy;
    0x99uy; 0x6fuy; 0xb9uy; 0x24uy; 0x27uy; 0xaeuy; 0x41uy; 0xe4uy; 0x64uy; 0x9buy; 0x93uy; 0x4cuy;
    0xa4uy; 0x95uy; 0x99uy; 0x1buy; 0x78uy; 0x52uy; 0xb8uy; 0x55uy
  ]

let test2_expected384 =
  [
    0x38uy; 0xb0uy; 0x60uy; 0xa7uy; 0x51uy; 0xacuy; 0x96uy; 0x38uy; 0x4cuy; 0xd9uy; 0x32uy; 0x7euy;
    0xb1uy; 0xb1uy; 0xe3uy; 0x6auy; 0x21uy; 0xfduy; 0xb7uy; 0x11uy; 0x14uy; 0xbeuy; 0x07uy; 0x43uy;
    0x4cuy; 0x0cuy; 0xc7uy; 0xbfuy; 0x63uy; 0xf6uy; 0xe1uy; 0xdauy; 0x27uy; 0x4euy; 0xdeuy; 0xbfuy;
    0xe7uy; 0x6fuy; 0x65uy; 0xfbuy; 0xd5uy; 0x1auy; 0xd2uy; 0xf1uy; 0x48uy; 0x98uy; 0xb9uy; 0x5buy
  ]

let test2_expected512 =
  [
    0xcfuy; 0x83uy; 0xe1uy; 0x35uy; 0x7euy; 0xefuy; 0xb8uy; 0xbduy; 0xf1uy; 0x54uy; 0x28uy; 0x50uy;
    0xd6uy; 0x6duy; 0x80uy; 0x07uy; 0xd6uy; 0x20uy; 0xe4uy; 0x05uy; 0x0buy; 0x57uy; 0x15uy; 0xdcuy;
    0x83uy; 0xf4uy; 0xa9uy; 0x21uy; 0xd3uy; 0x6cuy; 0xe9uy; 0xceuy; 0x47uy; 0xd0uy; 0xd1uy; 0x3cuy;
    0x5duy; 0x85uy; 0xf2uy; 0xb0uy; 0xffuy; 0x83uy; 0x18uy; 0xd2uy; 0x87uy; 0x7euy; 0xecuy; 0x2fuy;
    0x63uy; 0xb9uy; 0x31uy; 0xbduy; 0x47uy; 0x41uy; 0x7auy; 0x81uy; 0xa5uy; 0x38uy; 0x32uy; 0x7auy;
    0xf9uy; 0x27uy; 0xdauy; 0x3euy
  ]

//
// Test 3
//

let test3_plaintext =
  [
    0x61uy; 0x62uy; 0x63uy; 0x64uy; 0x62uy; 0x63uy; 0x64uy; 0x65uy; 0x63uy; 0x64uy; 0x65uy; 0x66uy;
    0x64uy; 0x65uy; 0x66uy; 0x67uy; 0x65uy; 0x66uy; 0x67uy; 0x68uy; 0x66uy; 0x67uy; 0x68uy; 0x69uy;
    0x67uy; 0x68uy; 0x69uy; 0x6auy; 0x68uy; 0x69uy; 0x6auy; 0x6buy; 0x69uy; 0x6auy; 0x6buy; 0x6cuy;
    0x6auy; 0x6buy; 0x6cuy; 0x6duy; 0x6buy; 0x6cuy; 0x6duy; 0x6euy; 0x6cuy; 0x6duy; 0x6euy; 0x6fuy;
    0x6duy; 0x6euy; 0x6fuy; 0x70uy; 0x6euy; 0x6fuy; 0x70uy; 0x71uy
  ]

let test3_expected224 =
  [
    0x75uy; 0x38uy; 0x8buy; 0x16uy; 0x51uy; 0x27uy; 0x76uy; 0xccuy; 0x5duy; 0xbauy; 0x5duy; 0xa1uy;
    0xfduy; 0x89uy; 0x01uy; 0x50uy; 0xb0uy; 0xc6uy; 0x45uy; 0x5cuy; 0xb4uy; 0xf5uy; 0x8buy; 0x19uy;
    0x52uy; 0x52uy; 0x25uy; 0x25uy
  ]

let test3_expected256 =
  [
    0x24uy; 0x8duy; 0x6auy; 0x61uy; 0xd2uy; 0x06uy; 0x38uy; 0xb8uy; 0xe5uy; 0xc0uy; 0x26uy; 0x93uy;
    0x0cuy; 0x3euy; 0x60uy; 0x39uy; 0xa3uy; 0x3cuy; 0xe4uy; 0x59uy; 0x64uy; 0xffuy; 0x21uy; 0x67uy;
    0xf6uy; 0xecuy; 0xeduy; 0xd4uy; 0x19uy; 0xdbuy; 0x06uy; 0xc1uy
  ]

let test3_expected384 =
  [
    0x33uy; 0x91uy; 0xfduy; 0xdduy; 0xfcuy; 0x8duy; 0xc7uy; 0x39uy; 0x37uy; 0x07uy; 0xa6uy; 0x5buy;
    0x1buy; 0x47uy; 0x09uy; 0x39uy; 0x7cuy; 0xf8uy; 0xb1uy; 0xd1uy; 0x62uy; 0xafuy; 0x05uy; 0xabuy;
    0xfeuy; 0x8fuy; 0x45uy; 0x0duy; 0xe5uy; 0xf3uy; 0x6buy; 0xc6uy; 0xb0uy; 0x45uy; 0x5auy; 0x85uy;
    0x20uy; 0xbcuy; 0x4euy; 0x6fuy; 0x5fuy; 0xe9uy; 0x5buy; 0x1fuy; 0xe3uy; 0xc8uy; 0x45uy; 0x2buy
  ]

let test3_expected512 =
  [
    0x20uy; 0x4auy; 0x8fuy; 0xc6uy; 0xdduy; 0xa8uy; 0x2fuy; 0x0auy; 0x0cuy; 0xeduy; 0x7buy; 0xebuy;
    0x8euy; 0x08uy; 0xa4uy; 0x16uy; 0x57uy; 0xc1uy; 0x6euy; 0xf4uy; 0x68uy; 0xb2uy; 0x28uy; 0xa8uy;
    0x27uy; 0x9buy; 0xe3uy; 0x31uy; 0xa7uy; 0x03uy; 0xc3uy; 0x35uy; 0x96uy; 0xfduy; 0x15uy; 0xc1uy;
    0x3buy; 0x1buy; 0x07uy; 0xf9uy; 0xaauy; 0x1duy; 0x3buy; 0xeauy; 0x57uy; 0x78uy; 0x9cuy; 0xa0uy;
    0x31uy; 0xaduy; 0x85uy; 0xc7uy; 0xa7uy; 0x1duy; 0xd7uy; 0x03uy; 0x54uy; 0xecuy; 0x63uy; 0x12uy;
    0x38uy; 0xcauy; 0x34uy; 0x45uy
  ]

//
// Test 4
//

let test4_plaintext =
  [
    0x61uy; 0x62uy; 0x63uy; 0x64uy; 0x65uy; 0x66uy; 0x67uy; 0x68uy; 0x62uy; 0x63uy; 0x64uy; 0x65uy;
    0x66uy; 0x67uy; 0x68uy; 0x69uy; 0x63uy; 0x64uy; 0x65uy; 0x66uy; 0x67uy; 0x68uy; 0x69uy; 0x6auy;
    0x64uy; 0x65uy; 0x66uy; 0x67uy; 0x68uy; 0x69uy; 0x6auy; 0x6buy; 0x65uy; 0x66uy; 0x67uy; 0x68uy;
    0x69uy; 0x6auy; 0x6buy; 0x6cuy; 0x66uy; 0x67uy; 0x68uy; 0x69uy; 0x6auy; 0x6buy; 0x6cuy; 0x6duy;
    0x67uy; 0x68uy; 0x69uy; 0x6auy; 0x6buy; 0x6cuy; 0x6duy; 0x6euy; 0x68uy; 0x69uy; 0x6auy; 0x6buy;
    0x6cuy; 0x6duy; 0x6euy; 0x6fuy; 0x69uy; 0x6auy; 0x6buy; 0x6cuy; 0x6duy; 0x6euy; 0x6fuy; 0x70uy;
    0x6auy; 0x6buy; 0x6cuy; 0x6duy; 0x6euy; 0x6fuy; 0x70uy; 0x71uy; 0x6buy; 0x6cuy; 0x6duy; 0x6euy;
    0x6fuy; 0x70uy; 0x71uy; 0x72uy; 0x6cuy; 0x6duy; 0x6euy; 0x6fuy; 0x70uy; 0x71uy; 0x72uy; 0x73uy;
    0x6duy; 0x6euy; 0x6fuy; 0x70uy; 0x71uy; 0x72uy; 0x73uy; 0x74uy; 0x6euy; 0x6fuy; 0x70uy; 0x71uy;
    0x72uy; 0x73uy; 0x74uy; 0x75uy
  ]

let test4_expected224 =
  [
    0xc9uy; 0x7cuy; 0xa9uy; 0xa5uy; 0x59uy; 0x85uy; 0x0cuy; 0xe9uy; 0x7auy; 0x04uy; 0xa9uy; 0x6duy;
    0xefuy; 0x6duy; 0x99uy; 0xa9uy; 0xe0uy; 0xe0uy; 0xe2uy; 0xabuy; 0x14uy; 0xe6uy; 0xb8uy; 0xdfuy;
    0x26uy; 0x5fuy; 0xc0uy; 0xb3uy
  ]

let test4_expected256 =
  [
    0xcfuy; 0x5buy; 0x16uy; 0xa7uy; 0x78uy; 0xafuy; 0x83uy; 0x80uy; 0x03uy; 0x6cuy; 0xe5uy; 0x9euy;
    0x7buy; 0x04uy; 0x92uy; 0x37uy; 0x0buy; 0x24uy; 0x9buy; 0x11uy; 0xe8uy; 0xf0uy; 0x7auy; 0x51uy;
    0xafuy; 0xacuy; 0x45uy; 0x03uy; 0x7auy; 0xfeuy; 0xe9uy; 0xd1uy
  ]

let test4_expected384 =
  [
    0x09uy; 0x33uy; 0x0cuy; 0x33uy; 0xf7uy; 0x11uy; 0x47uy; 0xe8uy; 0x3duy; 0x19uy; 0x2fuy; 0xc7uy;
    0x82uy; 0xcduy; 0x1buy; 0x47uy; 0x53uy; 0x11uy; 0x1buy; 0x17uy; 0x3buy; 0x3buy; 0x05uy; 0xd2uy;
    0x2fuy; 0xa0uy; 0x80uy; 0x86uy; 0xe3uy; 0xb0uy; 0xf7uy; 0x12uy; 0xfcuy; 0xc7uy; 0xc7uy; 0x1auy;
    0x55uy; 0x7euy; 0x2duy; 0xb9uy; 0x66uy; 0xc3uy; 0xe9uy; 0xfauy; 0x91uy; 0x74uy; 0x60uy; 0x39uy
  ]

let test4_expected512 =
  [
    0x8euy; 0x95uy; 0x9buy; 0x75uy; 0xdauy; 0xe3uy; 0x13uy; 0xdauy; 0x8cuy; 0xf4uy; 0xf7uy; 0x28uy;
    0x14uy; 0xfcuy; 0x14uy; 0x3fuy; 0x8fuy; 0x77uy; 0x79uy; 0xc6uy; 0xebuy; 0x9fuy; 0x7fuy; 0xa1uy;
    0x72uy; 0x99uy; 0xaeuy; 0xaduy; 0xb6uy; 0x88uy; 0x90uy; 0x18uy; 0x50uy; 0x1duy; 0x28uy; 0x9euy;
    0x49uy; 0x00uy; 0xf7uy; 0xe4uy; 0x33uy; 0x1buy; 0x99uy; 0xdeuy; 0xc4uy; 0xb5uy; 0x43uy; 0x3auy;
    0xc7uy; 0xd3uy; 0x29uy; 0xeeuy; 0xb6uy; 0xdduy; 0x26uy; 0x54uy; 0x5euy; 0x96uy; 0xe5uy; 0x5buy;
    0x87uy; 0x4buy; 0xe9uy; 0x09uy
  ]

//
// Test 5
//

let test5_expected224 = []

// let test5_expected256 = [
//   0xcduy; 0xc7uy; 0x6euy; 0x5cuy; 0x99uy; 0x14uy; 0xfbuy; 0x92uy;
//   0x81uy; 0xa1uy; 0xc7uy; 0xe2uy; 0x84uy; 0xd7uy; 0x3euy; 0x67uy;
//   0xf1uy; 0x80uy; 0x9auy; 0x48uy; 0xa4uy; 0x97uy; 0x20uy; 0x0euy;
//   0x04uy; 0x6duy; 0x39uy; 0xccuy; 0xc7uy; 0x11uy; 0x2cuy; 0xd0uy
// ]
//
// let test5_expected384 = [
//   0x9duy; 0x0euy; 0x18uy; 0x09uy; 0x71uy; 0x64uy; 0x74uy; 0xcbuy;
//   0x08uy; 0x6euy; 0x83uy; 0x4euy; 0x31uy; 0x0auy; 0x4auy; 0x1cuy;
//   0xeduy; 0x14uy; 0x9euy; 0x9cuy; 0x00uy; 0xf2uy; 0x48uy; 0x52uy;
//   0x79uy; 0x72uy; 0xceuy; 0xc5uy; 0x70uy; 0x4cuy; 0x2auy; 0x5buy;
//   0x07uy; 0xb8uy; 0xb3uy; 0xdcuy; 0x38uy; 0xecuy; 0xc4uy; 0xebuy;
//   0xaeuy; 0x97uy; 0xdduy; 0xd8uy; 0x7fuy; 0x3duy; 0x89uy; 0x85uy
// ]
//
// let test5_expected512 = [
//   0xe7uy; 0x18uy; 0x48uy; 0x3duy; 0x0cuy; 0xe7uy; 0x69uy; 0x64uy;
//   0x4euy; 0x2euy; 0x42uy; 0xc7uy; 0xbcuy; 0x15uy; 0xb4uy; 0x63uy;
//   0x8euy; 0x1fuy; 0x98uy; 0xb1uy; 0x3buy; 0x20uy; 0x44uy; 0x28uy;
//   0x56uy; 0x32uy; 0xa8uy; 0x03uy; 0xafuy; 0xa9uy; 0x73uy; 0xebuy;
//   0xdeuy; 0x0fuy; 0xf2uy; 0x44uy; 0x87uy; 0x7euy; 0xa6uy; 0x0auy;
//   0x4cuy; 0xb0uy; 0x43uy; 0x2cuy; 0xe5uy; 0x77uy; 0xc3uy; 0x1buy;
//   0xebuy; 0x00uy; 0x9cuy; 0x5cuy; 0x2cuy; 0x49uy; 0xaauy; 0x2euy;
//   0x4euy; 0xaduy; 0xb2uy; 0x17uy; 0xaduy; 0x8cuy; 0xc0uy; 0x9buy
// ]

open Spec.Agile.Hash
open Spec.Hash.Definitions

//
// Main
//

type vec =
  | Vec :
    a: hash_alg ->
    plain:
    list UInt8.t {norm [delta; iota; zeta; primops] (List.Tot.length plain <= max_input_length a) == true} ->
    hash:
    list UInt8.t {norm [delta; iota; zeta; primops] (List.Tot.length hash = hash_length a) == true} ->
    vec

let test_vectors: list vec =
  [
    Vec SHA2_224 test1_plaintext test1_expected224; Vec SHA2_224 test2_plaintext test2_expected224;
    Vec SHA2_224 test3_plaintext test3_expected224; Vec SHA2_224 test4_plaintext test4_expected224;
    Vec SHA2_256 test1_plaintext test1_expected256; Vec SHA2_256 test2_plaintext test2_expected256;
    Vec SHA2_256 test3_plaintext test3_expected256; Vec SHA2_256 test4_plaintext test4_expected256;
    Vec SHA2_384 test1_plaintext test1_expected384; Vec SHA2_384 test2_plaintext test2_expected384;
    Vec SHA2_384 test3_plaintext test3_expected384; Vec SHA2_384 test4_plaintext test4_expected384;
    Vec SHA2_512 test1_plaintext test1_expected512; Vec SHA2_512 test2_plaintext test2_expected512;
    Vec SHA2_512 test3_plaintext test3_expected512; Vec SHA2_512 test4_plaintext test4_expected512;
    (* MD5 tests from: ./make_md5_tests.sh *)
    (let plain: list FStar.UInt8.t = [] in
      let cipher: list FStar.UInt8.t =
        [
          0xd4uy; 0x1duy; 0x8cuy; 0xd9uy; 0x8fuy; 0x00uy; 0xb2uy; 0x04uy; 0xe9uy; 0x80uy; 0x09uy;
          0x98uy; 0xecuy; 0xf8uy; 0x42uy; 0x7euy
        ]
      in
      Vec MD5 plain cipher);
    (let plain: list FStar.UInt8.t = [0x61uy] in
      let cipher: list FStar.UInt8.t =
        [
          0x0cuy; 0xc1uy; 0x75uy; 0xb9uy; 0xc0uy; 0xf1uy; 0xb6uy; 0xa8uy; 0x31uy; 0xc3uy; 0x99uy;
          0xe2uy; 0x69uy; 0x77uy; 0x26uy; 0x61uy
        ]
      in
      Vec MD5 plain cipher);
    (let plain: list FStar.UInt8.t = [0x61uy; 0x62uy; 0x63uy] in
      let cipher: list FStar.UInt8.t =
        [
          0x90uy; 0x01uy; 0x50uy; 0x98uy; 0x3cuy; 0xd2uy; 0x4fuy; 0xb0uy; 0xd6uy; 0x96uy; 0x3fuy;
          0x7duy; 0x28uy; 0xe1uy; 0x7fuy; 0x72uy
        ]
      in
      Vec MD5 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x6duy; 0x65uy; 0x73uy; 0x73uy; 0x61uy; 0x67uy; 0x65uy; 0x20uy; 0x64uy; 0x69uy; 0x67uy;
          0x65uy; 0x73uy; 0x74uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xf9uy; 0x6buy; 0x69uy; 0x7duy; 0x7cuy; 0xb7uy; 0x93uy; 0x8duy; 0x52uy; 0x5auy; 0x2fuy;
          0x31uy; 0xaauy; 0xf1uy; 0x61uy; 0xd0uy
        ]
      in
      Vec MD5 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x61uy; 0x62uy; 0x63uy; 0x64uy; 0x65uy; 0x66uy; 0x67uy; 0x68uy; 0x69uy; 0x6auy; 0x6buy;
          0x6cuy; 0x6duy; 0x6euy; 0x6fuy; 0x70uy; 0x71uy; 0x72uy; 0x73uy; 0x74uy; 0x75uy; 0x76uy;
          0x77uy; 0x78uy; 0x79uy; 0x7auy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xc3uy; 0xfcuy; 0xd3uy; 0xd7uy; 0x61uy; 0x92uy; 0xe4uy; 0x00uy; 0x7duy; 0xfbuy; 0x49uy;
          0x6cuy; 0xcauy; 0x67uy; 0xe1uy; 0x3buy
        ]
      in
      Vec MD5 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x41uy; 0x42uy; 0x43uy; 0x44uy; 0x45uy; 0x46uy; 0x47uy; 0x48uy; 0x49uy; 0x4auy; 0x4buy;
          0x4cuy; 0x4duy; 0x4euy; 0x4fuy; 0x50uy; 0x51uy; 0x52uy; 0x53uy; 0x54uy; 0x55uy; 0x56uy;
          0x57uy; 0x58uy; 0x59uy; 0x5auy; 0x61uy; 0x62uy; 0x63uy; 0x64uy; 0x65uy; 0x66uy; 0x67uy;
          0x68uy; 0x69uy; 0x6auy; 0x6buy; 0x6cuy; 0x6duy; 0x6euy; 0x6fuy; 0x70uy; 0x71uy; 0x72uy;
          0x73uy; 0x74uy; 0x75uy; 0x76uy; 0x77uy; 0x78uy; 0x79uy; 0x7auy; 0x30uy; 0x31uy; 0x32uy;
          0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy; 0x38uy; 0x39uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xd1uy; 0x74uy; 0xabuy; 0x98uy; 0xd2uy; 0x77uy; 0xd9uy; 0xf5uy; 0xa5uy; 0x61uy; 0x1cuy;
          0x2cuy; 0x9fuy; 0x41uy; 0x9duy; 0x9fuy
        ]
      in
      Vec MD5 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x31uy; 0x32uy; 0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy; 0x38uy; 0x39uy; 0x30uy; 0x31uy;
          0x32uy; 0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy; 0x38uy; 0x39uy; 0x30uy; 0x31uy; 0x32uy;
          0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy; 0x38uy; 0x39uy; 0x30uy; 0x31uy; 0x32uy; 0x33uy;
          0x34uy; 0x35uy; 0x36uy; 0x37uy; 0x38uy; 0x39uy; 0x30uy; 0x31uy; 0x32uy; 0x33uy; 0x34uy;
          0x35uy; 0x36uy; 0x37uy; 0x38uy; 0x39uy; 0x30uy; 0x31uy; 0x32uy; 0x33uy; 0x34uy; 0x35uy;
          0x36uy; 0x37uy; 0x38uy; 0x39uy; 0x30uy; 0x31uy; 0x32uy; 0x33uy; 0x34uy; 0x35uy; 0x36uy;
          0x37uy; 0x38uy; 0x39uy; 0x30uy; 0x31uy; 0x32uy; 0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy;
          0x38uy; 0x39uy; 0x30uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x57uy; 0xeduy; 0xf4uy; 0xa2uy; 0x2buy; 0xe3uy; 0xc9uy; 0x55uy; 0xacuy; 0x49uy; 0xdauy;
          0x2euy; 0x21uy; 0x07uy; 0xb6uy; 0x7auy
        ]
      in
      Vec MD5 plain cipher);
    (* SHA1 tests from: ./make_sha1_tests.sh *)
    (let plain: list FStar.UInt8.t = [] in
      let cipher: list FStar.UInt8.t =
        [
          0xdauy; 0x39uy; 0xa3uy; 0xeeuy; 0x5euy; 0x6buy; 0x4buy; 0x0duy; 0x32uy; 0x55uy; 0xbfuy;
          0xefuy; 0x95uy; 0x60uy; 0x18uy; 0x90uy; 0xafuy; 0xd8uy; 0x07uy; 0x09uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t = [0x36uy] in
      let cipher: list FStar.UInt8.t =
        [
          0xc1uy; 0xdfuy; 0xd9uy; 0x6euy; 0xeauy; 0x8cuy; 0xc2uy; 0xb6uy; 0x27uy; 0x85uy; 0x27uy;
          0x5buy; 0xcauy; 0x38uy; 0xacuy; 0x26uy; 0x12uy; 0x56uy; 0xe2uy; 0x78uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t = [0x19uy; 0x5auy] in
      let cipher: list FStar.UInt8.t =
        [
          0x0auy; 0x1cuy; 0x2duy; 0x55uy; 0x5buy; 0xbeuy; 0x43uy; 0x1auy; 0xd6uy; 0x28uy; 0x8auy;
          0xf5uy; 0xa5uy; 0x4fuy; 0x93uy; 0xe0uy; 0x44uy; 0x9cuy; 0x92uy; 0x32uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t = [0xdfuy; 0x4buy; 0xd2uy] in
      let cipher: list FStar.UInt8.t =
        [
          0xbfuy; 0x36uy; 0xeduy; 0x5duy; 0x74uy; 0x72uy; 0x7duy; 0xfduy; 0x5duy; 0x78uy; 0x54uy;
          0xecuy; 0x6buy; 0x1duy; 0x49uy; 0x46uy; 0x8duy; 0x8euy; 0xe8uy; 0xaauy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t = [0x54uy; 0x9euy; 0x95uy; 0x9euy] in
      let cipher: list FStar.UInt8.t =
        [
          0xb7uy; 0x8buy; 0xaeuy; 0x6duy; 0x14uy; 0x33uy; 0x8fuy; 0xfcuy; 0xcfuy; 0xd5uy; 0xd5uy;
          0xb5uy; 0x67uy; 0x4auy; 0x27uy; 0x5fuy; 0x6euy; 0xf9uy; 0xc7uy; 0x17uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t = [0xf7uy; 0xfbuy; 0x1buy; 0xe2uy; 0x05uy] in
      let cipher: list FStar.UInt8.t =
        [
          0x60uy; 0xb7uy; 0xd5uy; 0xbbuy; 0x56uy; 0x0auy; 0x1auy; 0xcfuy; 0x6fuy; 0xa4uy; 0x57uy;
          0x21uy; 0xbduy; 0x0auy; 0xbbuy; 0x41uy; 0x9auy; 0x84uy; 0x1auy; 0x89uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t = [0xc0uy; 0xe5uy; 0xabuy; 0xeauy; 0xeauy; 0x63uy] in
      let cipher: list FStar.UInt8.t =
        [
          0xa6uy; 0xd3uy; 0x38uy; 0x45uy; 0x97uy; 0x80uy; 0xc0uy; 0x83uy; 0x63uy; 0x09uy; 0x0fuy;
          0xd8uy; 0xfcuy; 0x7duy; 0x28uy; 0xdcuy; 0x80uy; 0xe8uy; 0xe0uy; 0x1fuy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t = [0x63uy; 0xbfuy; 0xc1uy; 0xeduy; 0x7fuy; 0x78uy; 0xabuy] in
      let cipher: list FStar.UInt8.t =
        [
          0x86uy; 0x03uy; 0x28uy; 0xd8uy; 0x05uy; 0x09uy; 0x50uy; 0x0cuy; 0x17uy; 0x83uy; 0x16uy;
          0x9euy; 0xbfuy; 0x0buy; 0xa0uy; 0xc4uy; 0xb9uy; 0x4duy; 0xa5uy; 0xe5uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [0x7euy; 0x3duy; 0x7buy; 0x3euy; 0xaduy; 0xa9uy; 0x88uy; 0x66uy]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x24uy; 0xa2uy; 0xc3uy; 0x4buy; 0x97uy; 0x63uy; 0x05uy; 0x27uy; 0x7cuy; 0xe5uy; 0x8cuy;
          0x2fuy; 0x42uy; 0xd5uy; 0x09uy; 0x20uy; 0x31uy; 0x57uy; 0x25uy; 0x20uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [0x9euy; 0x61uy; 0xe5uy; 0x5duy; 0x9euy; 0xd3uy; 0x7buy; 0x1cuy; 0x20uy]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x41uy; 0x1cuy; 0xceuy; 0xe1uy; 0xf6uy; 0xe3uy; 0x67uy; 0x7duy; 0xf1uy; 0x26uy; 0x98uy;
          0x41uy; 0x1euy; 0xb0uy; 0x9duy; 0x3fuy; 0xf5uy; 0x80uy; 0xafuy; 0x97uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [0x97uy; 0x77uy; 0xcfuy; 0x90uy; 0xdduy; 0x7cuy; 0x7euy; 0x86uy; 0x35uy; 0x06uy]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x05uy; 0xc9uy; 0x15uy; 0xb5uy; 0xeduy; 0x4euy; 0x4cuy; 0x4auy; 0xffuy; 0xfcuy; 0x20uy;
          0x29uy; 0x61uy; 0xf3uy; 0x17uy; 0x43uy; 0x71uy; 0xe9uy; 0x0buy; 0x5cuy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [0x4euy; 0xb0uy; 0x8cuy; 0x9euy; 0x68uy; 0x3cuy; 0x94uy; 0xbeuy; 0xa0uy; 0x0duy; 0xfauy]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xafuy; 0x32uy; 0x0buy; 0x42uy; 0xd7uy; 0x78uy; 0x5cuy; 0xa6uy; 0xc8uy; 0xdduy; 0x22uy;
          0x04uy; 0x63uy; 0xbeuy; 0x23uy; 0xa2uy; 0xd2uy; 0xcbuy; 0x5auy; 0xfcuy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x09uy; 0x38uy; 0xf2uy; 0xe2uy; 0xebuy; 0xb6uy; 0x4fuy; 0x8auy; 0xf8uy; 0xbbuy; 0xfcuy;
          0x91uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x9fuy; 0x4euy; 0x66uy; 0xb6uy; 0xceuy; 0xeauy; 0x40uy; 0xdcuy; 0xf4uy; 0xb9uy; 0x16uy;
          0x6cuy; 0x28uy; 0xf1uy; 0xc8uy; 0x84uy; 0x74uy; 0x14uy; 0x1duy; 0xa9uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x74uy; 0xc9uy; 0x99uy; 0x6duy; 0x14uy; 0xe8uy; 0x7duy; 0x3euy; 0x6cuy; 0xbeuy; 0xa7uy;
          0x02uy; 0x9duy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xe6uy; 0xc4uy; 0x36uy; 0x3cuy; 0x08uy; 0x52uy; 0x95uy; 0x19uy; 0x91uy; 0x05uy; 0x7fuy;
          0x40uy; 0xdeuy; 0x27uy; 0xecuy; 0x08uy; 0x90uy; 0x46uy; 0x6fuy; 0x01uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x51uy; 0xdcuy; 0xa5uy; 0xc0uy; 0xf8uy; 0xe5uy; 0xd4uy; 0x95uy; 0x96uy; 0xf3uy; 0x2duy;
          0x3euy; 0xb8uy; 0x74uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x04uy; 0x6auy; 0x7buy; 0x39uy; 0x6cuy; 0x01uy; 0x37uy; 0x9auy; 0x68uy; 0x4auy; 0x89uy;
          0x45uy; 0x58uy; 0x77uy; 0x9buy; 0x07uy; 0xd8uy; 0xc7uy; 0xdauy; 0x20uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x3auy; 0x36uy; 0xeauy; 0x49uy; 0x68uy; 0x48uy; 0x20uy; 0xa2uy; 0xaduy; 0xc7uy; 0xfcuy;
          0x41uy; 0x75uy; 0xbauy; 0x78uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xd5uy; 0x8auy; 0x26uy; 0x2euy; 0xe7uy; 0xb6uy; 0x57uy; 0x7cuy; 0x07uy; 0x22uy; 0x8euy;
          0x71uy; 0xaeuy; 0x9buy; 0x3euy; 0x04uy; 0xc8uy; 0xabuy; 0xcduy; 0xa9uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x35uy; 0x52uy; 0x69uy; 0x4cuy; 0xdfuy; 0x66uy; 0x3fuy; 0xd9uy; 0x4buy; 0x22uy; 0x47uy;
          0x47uy; 0xacuy; 0x40uy; 0x6auy; 0xafuy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xa1uy; 0x50uy; 0xdeuy; 0x92uy; 0x74uy; 0x54uy; 0x20uy; 0x2duy; 0x94uy; 0xe6uy; 0x56uy;
          0xdeuy; 0x4cuy; 0x7cuy; 0x0cuy; 0xa6uy; 0x91uy; 0xdeuy; 0x95uy; 0x5duy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0xf2uy; 0x16uy; 0xa1uy; 0xcbuy; 0xdeuy; 0x24uy; 0x46uy; 0xb1uy; 0xeduy; 0xf4uy; 0x1euy;
          0x93uy; 0x48uy; 0x1duy; 0x33uy; 0xe2uy; 0xeduy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x35uy; 0xa4uy; 0xb3uy; 0x9fuy; 0xefuy; 0x56uy; 0x0euy; 0x7euy; 0xa6uy; 0x12uy; 0x46uy;
          0x67uy; 0x6euy; 0x1buy; 0x7euy; 0x13uy; 0xd5uy; 0x87uy; 0xbeuy; 0x30uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0xa3uy; 0xcfuy; 0x71uy; 0x4buy; 0xf1uy; 0x12uy; 0x64uy; 0x7euy; 0x72uy; 0x7euy; 0x8cuy;
          0xfduy; 0x46uy; 0x49uy; 0x9auy; 0xcduy; 0x35uy; 0xa6uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x7cuy; 0xe6uy; 0x9buy; 0x1auy; 0xcduy; 0xceuy; 0x52uy; 0xeauy; 0x7duy; 0xbduy; 0x38uy;
          0x25uy; 0x31uy; 0xfauy; 0x1auy; 0x83uy; 0xdfuy; 0x13uy; 0xcauy; 0xe7uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x14uy; 0x8duy; 0xe6uy; 0x40uy; 0xf3uy; 0xc1uy; 0x15uy; 0x91uy; 0xa6uy; 0xf8uy; 0xc5uy;
          0xc4uy; 0x86uy; 0x32uy; 0xc5uy; 0xfbuy; 0x79uy; 0xd3uy; 0xb7uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xb4uy; 0x7buy; 0xe2uy; 0xc6uy; 0x41uy; 0x24uy; 0xfauy; 0x9auy; 0x12uy; 0x4auy; 0x88uy;
          0x7auy; 0xf9uy; 0x55uy; 0x1auy; 0x74uy; 0x35uy; 0x4cuy; 0xa4uy; 0x11uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x63uy; 0xa3uy; 0xccuy; 0x83uy; 0xfduy; 0x1euy; 0xc1uy; 0xb6uy; 0x68uy; 0x0euy; 0x99uy;
          0x74uy; 0xa0uy; 0x51uy; 0x4euy; 0x1auy; 0x9euy; 0xceuy; 0xbbuy; 0x6auy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x8buy; 0xb8uy; 0xc0uy; 0xd8uy; 0x15uy; 0xa9uy; 0xc6uy; 0x8auy; 0x1duy; 0x29uy; 0x10uy;
          0xf3uy; 0x9duy; 0x94uy; 0x26uy; 0x03uy; 0xd8uy; 0x07uy; 0xfbuy; 0xccuy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x87uy; 0x5auy; 0x90uy; 0x90uy; 0x9auy; 0x8auy; 0xfcuy; 0x92uy; 0xfbuy; 0x70uy; 0x70uy;
          0x04uy; 0x7euy; 0x9duy; 0x08uy; 0x1euy; 0xc9uy; 0x2fuy; 0x3duy; 0x08uy; 0xb8uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xb4uy; 0x86uy; 0xf8uy; 0x7fuy; 0xb8uy; 0x33uy; 0xebuy; 0xf0uy; 0x32uy; 0x83uy; 0x93uy;
          0x12uy; 0x86uy; 0x46uy; 0xa6uy; 0xf6uy; 0xe6uy; 0x60uy; 0xfcuy; 0xb1uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x44uy; 0x4buy; 0x25uy; 0xf9uy; 0xc9uy; 0x25uy; 0x9duy; 0xc2uy; 0x17uy; 0x77uy; 0x2cuy;
          0xc4uy; 0x47uy; 0x8cuy; 0x44uy; 0xb6uy; 0xfeuy; 0xffuy; 0x62uy; 0x35uy; 0x36uy; 0x73uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x76uy; 0x15uy; 0x93uy; 0x68uy; 0xf9uy; 0x9duy; 0xecuy; 0xe3uy; 0x0auy; 0xaduy; 0xcfuy;
          0xb9uy; 0xb7uy; 0xb4uy; 0x1duy; 0xabuy; 0x33uy; 0x68uy; 0x88uy; 0x58uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x48uy; 0x73uy; 0x51uy; 0xc8uy; 0xa5uy; 0xf4uy; 0x40uy; 0xe4uy; 0xd0uy; 0x33uy; 0x86uy;
          0x48uy; 0x3duy; 0x5fuy; 0xe7uy; 0xbbuy; 0x66uy; 0x9duy; 0x41uy; 0xaduy; 0xcbuy; 0xfduy;
          0xb7uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xdbuy; 0xc1uy; 0xcbuy; 0x57uy; 0x5cuy; 0xe6uy; 0xaeuy; 0xb9uy; 0xdcuy; 0x4euy; 0xbfuy;
          0x0fuy; 0x84uy; 0x3buy; 0xa8uy; 0xaeuy; 0xb1uy; 0x45uy; 0x1euy; 0x89uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x46uy; 0xb0uy; 0x61uy; 0xefuy; 0x13uy; 0x2buy; 0x87uy; 0xf6uy; 0xd3uy; 0xb0uy; 0xeeuy;
          0x24uy; 0x62uy; 0xf6uy; 0x7duy; 0x91uy; 0x09uy; 0x77uy; 0xdauy; 0x20uy; 0xaeuy; 0xd1uy;
          0x37uy; 0x05uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xd7uy; 0xa9uy; 0x82uy; 0x89uy; 0x67uy; 0x90uy; 0x05uy; 0xebuy; 0x93uy; 0x0auy; 0xb7uy;
          0x5euy; 0xfduy; 0x8fuy; 0x65uy; 0x0fuy; 0x99uy; 0x1euy; 0xe9uy; 0x52uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x38uy; 0x42uy; 0xb6uy; 0x13uy; 0x7buy; 0xb9uy; 0xd2uy; 0x7fuy; 0x3cuy; 0xa5uy; 0xbauy;
          0xfeuy; 0x5buy; 0xbbuy; 0x62uy; 0x85uy; 0x83uy; 0x44uy; 0xfeuy; 0x4buy; 0xa5uy; 0xc4uy;
          0x15uy; 0x89uy; 0xa5uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xfduy; 0xa2uy; 0x6fuy; 0xa9uy; 0xb4uy; 0x87uy; 0x4auy; 0xb7uy; 0x01uy; 0xeduy; 0x0buy;
          0xb6uy; 0x4duy; 0x13uy; 0x4fuy; 0x89uy; 0xb9uy; 0xc4uy; 0xccuy; 0x50uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x44uy; 0xd9uy; 0x1duy; 0x3duy; 0x46uy; 0x5auy; 0x41uy; 0x11uy; 0x46uy; 0x2buy; 0xa0uy;
          0xc7uy; 0xecuy; 0x22uy; 0x3duy; 0xa6uy; 0x73uy; 0x5fuy; 0x4fuy; 0x52uy; 0x00uy; 0x45uy;
          0x3cuy; 0xf1uy; 0x32uy; 0xc3uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xc2uy; 0xffuy; 0x7cuy; 0xcduy; 0xe1uy; 0x43uy; 0xc8uy; 0xf0uy; 0x60uy; 0x1fuy; 0x69uy;
          0x74uy; 0xb1uy; 0x90uy; 0x3euy; 0xb8uy; 0xd5uy; 0x74uy; 0x1buy; 0x6euy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0xccuy; 0xe7uy; 0x3fuy; 0x2euy; 0xabuy; 0xcbuy; 0x52uy; 0xf7uy; 0x85uy; 0xd5uy; 0xa6uy;
          0xdfuy; 0x63uy; 0xc0uy; 0xa1uy; 0x05uy; 0xf3uy; 0x4auy; 0x91uy; 0xcauy; 0x23uy; 0x7fuy;
          0xe5uy; 0x34uy; 0xeeuy; 0x39uy; 0x9duy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x64uy; 0x3cuy; 0x9duy; 0xc2uy; 0x0auy; 0x92uy; 0x96uy; 0x08uy; 0xf6uy; 0xcauy; 0xa9uy;
          0x70uy; 0x9duy; 0x84uy; 0x3cuy; 0xa6uy; 0xfauy; 0x7auy; 0x76uy; 0xf4uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x66uy; 0x4euy; 0x6euy; 0x79uy; 0x46uy; 0x83uy; 0x92uy; 0x03uy; 0x03uy; 0x7auy; 0x65uy;
          0xa1uy; 0x21uy; 0x74uy; 0xb2uy; 0x44uy; 0xdeuy; 0x8cuy; 0xbcuy; 0x6euy; 0xc3uy; 0xf5uy;
          0x78uy; 0x96uy; 0x7auy; 0x84uy; 0xf9uy; 0xceuy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x50uy; 0x9euy; 0xf7uy; 0x87uy; 0x34uy; 0x3duy; 0x5buy; 0x5auy; 0x26uy; 0x92uy; 0x29uy;
          0xb9uy; 0x61uy; 0xb9uy; 0x62uy; 0x41uy; 0x86uy; 0x4auy; 0x3duy; 0x74uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x95uy; 0x97uy; 0xf7uy; 0x14uy; 0xb2uy; 0xe4uy; 0x5euy; 0x33uy; 0x99uy; 0xa7uy; 0xf0uy;
          0x2auy; 0xecuy; 0x44uy; 0x92uy; 0x1buy; 0xd7uy; 0x8buy; 0xe0uy; 0xfeuy; 0xfeuy; 0xe0uy;
          0xc5uy; 0xe9uy; 0xb4uy; 0x99uy; 0x48uy; 0x8fuy; 0x6euy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xb6uy; 0x1cuy; 0xe5uy; 0x38uy; 0xf1uy; 0xa1uy; 0xe6uy; 0xc9uy; 0x04uy; 0x32uy; 0xb2uy;
          0x33uy; 0xd7uy; 0xafuy; 0x5buy; 0x65uy; 0x24uy; 0xebuy; 0xfbuy; 0xe3uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x75uy; 0xc5uy; 0xaduy; 0x1fuy; 0x3cuy; 0xbduy; 0x22uy; 0xe8uy; 0xa9uy; 0x5fuy; 0xc3uy;
          0xb0uy; 0x89uy; 0x52uy; 0x67uy; 0x88uy; 0xfbuy; 0x4euy; 0xbcuy; 0xeeuy; 0xd3uy; 0xe7uy;
          0xd4uy; 0x44uy; 0x3duy; 0xa6uy; 0xe0uy; 0x81uy; 0xa3uy; 0x5euy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x5buy; 0x7buy; 0x94uy; 0x07uy; 0x6buy; 0x2fuy; 0xc2uy; 0x0duy; 0x6auy; 0xdbuy; 0x82uy;
          0x47uy; 0x9euy; 0x6buy; 0x28uy; 0xd0uy; 0x7cuy; 0x90uy; 0x2buy; 0x75uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0xdduy; 0x24uy; 0x5buy; 0xffuy; 0xe6uy; 0xa6uy; 0x38uy; 0x80uy; 0x66uy; 0x67uy; 0x76uy;
          0x83uy; 0x60uy; 0xa9uy; 0x5duy; 0x05uy; 0x74uy; 0xe1uy; 0xa0uy; 0xbduy; 0x0duy; 0x18uy;
          0x32uy; 0x9fuy; 0xdbuy; 0x91uy; 0x5cuy; 0xa4uy; 0x84uy; 0xacuy; 0x0duy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x60uy; 0x66uy; 0xdbuy; 0x99uy; 0xfcuy; 0x35uy; 0x89uy; 0x52uy; 0xcfuy; 0x7fuy; 0xb0uy;
          0xecuy; 0x4duy; 0x89uy; 0xcbuy; 0x01uy; 0x58uy; 0xeduy; 0x91uy; 0xd7uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x03uy; 0x21uy; 0x79uy; 0x4buy; 0x73uy; 0x94uy; 0x18uy; 0xc2uy; 0x4euy; 0x7cuy; 0x2euy;
          0x56uy; 0x52uy; 0x74uy; 0x79uy; 0x1cuy; 0x4buy; 0xe7uy; 0x49uy; 0x75uy; 0x2auy; 0xd2uy;
          0x34uy; 0xeduy; 0x56uy; 0xcbuy; 0x0auy; 0x63uy; 0x47uy; 0x43uy; 0x0cuy; 0x6buy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xb8uy; 0x99uy; 0x62uy; 0xc9uy; 0x4duy; 0x60uy; 0xf6uy; 0xa3uy; 0x32uy; 0xfduy; 0x60uy;
          0xf6uy; 0xf0uy; 0x7duy; 0x4fuy; 0x03uy; 0x2auy; 0x58uy; 0x6buy; 0x76uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x4cuy; 0x3duy; 0xcfuy; 0x95uy; 0xc2uy; 0xf0uy; 0xb5uy; 0x25uy; 0x8cuy; 0x65uy; 0x1fuy;
          0xcduy; 0x1duy; 0x51uy; 0xbduy; 0x10uy; 0x42uy; 0x5duy; 0x62uy; 0x03uy; 0x06uy; 0x7duy;
          0x07uy; 0x48uy; 0xd3uy; 0x7duy; 0x13uy; 0x40uy; 0xd9uy; 0xdduy; 0xdauy; 0x7duy; 0xb3uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x17uy; 0xbduy; 0xa8uy; 0x99uy; 0xc1uy; 0x3duy; 0x35uy; 0x41uy; 0x3duy; 0x25uy; 0x46uy;
          0x21uy; 0x2buy; 0xcduy; 0x8auy; 0x93uy; 0xceuy; 0xb0uy; 0x65uy; 0x7buy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0xb8uy; 0xd1uy; 0x25uy; 0x82uy; 0xd2uy; 0x5buy; 0x45uy; 0x29uy; 0x0auy; 0x6euy; 0x1buy;
          0xb9uy; 0x5duy; 0xa4uy; 0x29uy; 0xbeuy; 0xfcuy; 0xfduy; 0xbfuy; 0x5buy; 0x4duy; 0xd4uy;
          0x1cuy; 0xdfuy; 0x33uy; 0x11uy; 0xd6uy; 0x98uy; 0x8fuy; 0xa1uy; 0x7cuy; 0xecuy; 0x07uy;
          0x23uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xbauy; 0xdcuy; 0xdduy; 0x53uy; 0xfduy; 0xc1uy; 0x44uy; 0xb8uy; 0xbfuy; 0x2cuy; 0xc1uy;
          0xe6uy; 0x4duy; 0x10uy; 0xf6uy; 0x76uy; 0xeeuy; 0xbeuy; 0x66uy; 0xeduy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x6fuy; 0xdauy; 0x97uy; 0x52uy; 0x7auy; 0x66uy; 0x25uy; 0x52uy; 0xbeuy; 0x15uy; 0xefuy;
          0xaeuy; 0xbauy; 0x32uy; 0xa3uy; 0xaeuy; 0xa4uy; 0xeduy; 0x44uy; 0x9auy; 0xbbuy; 0x5cuy;
          0x1euy; 0xd8uy; 0xd9uy; 0xbfuy; 0xffuy; 0x54uy; 0x47uy; 0x08uy; 0xa4uy; 0x25uy; 0xd6uy;
          0x9buy; 0x72uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x01uy; 0xb4uy; 0x64uy; 0x61uy; 0x80uy; 0xf1uy; 0xf6uy; 0xd2uy; 0xe0uy; 0x6buy; 0xbeuy;
          0x22uy; 0xc2uy; 0x0euy; 0x50uy; 0x03uy; 0x03uy; 0x22uy; 0x67uy; 0x3auy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x09uy; 0xfauy; 0x27uy; 0x92uy; 0xacuy; 0xbbuy; 0x24uy; 0x17uy; 0xe8uy; 0xeduy; 0x26uy;
          0x90uy; 0x41uy; 0xccuy; 0x03uy; 0xc7uy; 0x70uy; 0x06uy; 0x46uy; 0x6euy; 0x6euy; 0x7auy;
          0xe0uy; 0x02uy; 0xcfuy; 0x3fuy; 0x1auy; 0xf5uy; 0x51uy; 0xe8uy; 0xceuy; 0x0buy; 0xb5uy;
          0x06uy; 0xd7uy; 0x05uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x10uy; 0x01uy; 0x6duy; 0xc3uy; 0xa2uy; 0x71uy; 0x9fuy; 0x90uy; 0x34uy; 0xffuy; 0xccuy;
          0x68uy; 0x94uy; 0x26uy; 0xd2uy; 0x82uy; 0x92uy; 0xc4uy; 0x2fuy; 0xc9uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x5euy; 0xfauy; 0x29uy; 0x87uy; 0xdauy; 0x0buy; 0xafuy; 0x0auy; 0x54uy; 0xd8uy; 0xd7uy;
          0x28uy; 0x79uy; 0x2buy; 0xcfuy; 0xa7uy; 0x07uy; 0xa1uy; 0x57uy; 0x98uy; 0xdcuy; 0x66uy;
          0x74uy; 0x37uy; 0x54uy; 0x40uy; 0x69uy; 0x14uy; 0xd1uy; 0xcfuy; 0xe3uy; 0x70uy; 0x9buy;
          0x13uy; 0x74uy; 0xeauy; 0xebuy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x9fuy; 0x42uy; 0xfauy; 0x2buy; 0xceuy; 0x6euy; 0xf0uy; 0x21uy; 0xd9uy; 0x3cuy; 0x6buy;
          0x2duy; 0x90uy; 0x22uy; 0x73uy; 0x79uy; 0x7euy; 0x42uy; 0x65uy; 0x35uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x28uy; 0x36uy; 0xdeuy; 0x99uy; 0xc0uy; 0xf6uy; 0x41uy; 0xcduy; 0x55uy; 0xe8uy; 0x9fuy;
          0x5auy; 0xf7uy; 0x66uy; 0x38uy; 0x94uy; 0x7buy; 0x82uy; 0x27uy; 0x37uy; 0x7euy; 0xf8uy;
          0x8buy; 0xfbuy; 0xa6uy; 0x62uy; 0xe5uy; 0x68uy; 0x2buy; 0xabuy; 0xc1uy; 0xecuy; 0x96uy;
          0xc6uy; 0x99uy; 0x2buy; 0xc9uy; 0xa0uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xcduy; 0xf4uy; 0x8buy; 0xacuy; 0xbfuy; 0xf6uy; 0xf6uy; 0x15uy; 0x25uy; 0x15uy; 0x32uy;
          0x3fuy; 0x9buy; 0x43uy; 0xa2uy; 0x86uy; 0xe0uy; 0xcbuy; 0x81uy; 0x13uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x42uy; 0x14uy; 0x3auy; 0x2buy; 0x9euy; 0x1duy; 0x0buy; 0x35uy; 0x4duy; 0xf3uy; 0x26uy;
          0x4duy; 0x08uy; 0xf7uy; 0xb6uy; 0x02uy; 0xf5uy; 0x4auy; 0xaduy; 0x92uy; 0x2auy; 0x3duy;
          0x63uy; 0x00uy; 0x6duy; 0x09uy; 0x7fuy; 0x68uy; 0x3duy; 0xc1uy; 0x1buy; 0x90uy; 0x17uy;
          0x84uy; 0x23uy; 0xbfuy; 0xf2uy; 0xf7uy; 0xfeuy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xb8uy; 0x8fuy; 0xb7uy; 0x52uy; 0x74uy; 0xb9uy; 0xb0uy; 0xfduy; 0x57uy; 0xc0uy; 0x04uy;
          0x59uy; 0x88uy; 0xcfuy; 0xceuy; 0xf6uy; 0xc3uy; 0xceuy; 0x65uy; 0x54uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0xebuy; 0x60uy; 0xc2uy; 0x8auy; 0xd8uy; 0xaeuy; 0xdauy; 0x80uy; 0x7duy; 0x69uy; 0xebuy;
          0xc8uy; 0x75uy; 0x52uy; 0x02uy; 0x4auy; 0xd8uy; 0xacuy; 0xa6uy; 0x82uy; 0x04uy; 0xf1uy;
          0xbcuy; 0xd2uy; 0x9duy; 0xc5uy; 0xa8uy; 0x1duy; 0xd2uy; 0x28uy; 0xb5uy; 0x91uy; 0xe2uy;
          0xefuy; 0xb7uy; 0xc4uy; 0xdfuy; 0x75uy; 0xefuy; 0x03uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xc0uy; 0x6duy; 0x3auy; 0x6auy; 0x12uy; 0xd9uy; 0xe8uy; 0xdbuy; 0x62uy; 0xe8uy; 0xcfuy;
          0xf4uy; 0x0cuy; 0xa2uy; 0x38uy; 0x20uy; 0xd6uy; 0x1duy; 0x8auy; 0xa7uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x7duy; 0xe4uy; 0xbauy; 0x85uy; 0xecuy; 0x54uy; 0x74uy; 0x7cuy; 0xdcuy; 0x42uy; 0xb1uy;
          0xf2uy; 0x35uy; 0x46uy; 0xb7uy; 0xe4uy; 0x90uy; 0xe3uy; 0x12uy; 0x80uy; 0xf0uy; 0x66uy;
          0xe5uy; 0x2fuy; 0xacuy; 0x11uy; 0x7fuy; 0xd3uy; 0xb0uy; 0x79uy; 0x2euy; 0x4duy; 0xe6uy;
          0x2duy; 0x58uy; 0x43uy; 0xeeuy; 0x98uy; 0xc7uy; 0x20uy; 0x15uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x6euy; 0x40uy; 0xf9uy; 0xe8uy; 0x3auy; 0x4buy; 0xe9uy; 0x38uy; 0x74uy; 0xbcuy; 0x97uy;
          0xcduy; 0xebuy; 0xb8uy; 0xdauy; 0x68uy; 0x89uy; 0xaeuy; 0x2cuy; 0x7auy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0xe7uy; 0x06uy; 0x53uy; 0x63uy; 0x7buy; 0xc5uy; 0xe3uy; 0x88uy; 0xccuy; 0xd8uy; 0xdcuy;
          0x44uy; 0xe5uy; 0xeauy; 0xceuy; 0x36uy; 0xf7uy; 0x39uy; 0x8fuy; 0x2buy; 0xacuy; 0x99uy;
          0x30uy; 0x42uy; 0xb9uy; 0xbcuy; 0x2fuy; 0x4fuy; 0xb3uy; 0xb0uy; 0xeeuy; 0x7euy; 0x23uy;
          0xa9uy; 0x64uy; 0x39uy; 0xdcuy; 0x01uy; 0x13uy; 0x4buy; 0x8cuy; 0x7duy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x3euy; 0xfcuy; 0x94uy; 0x0cuy; 0x31uy; 0x2euy; 0xf0uy; 0xdfuy; 0xd4uy; 0xe1uy; 0x14uy;
          0x38uy; 0x12uy; 0x24uy; 0x8duy; 0xb8uy; 0x95uy; 0x42uy; 0xf6uy; 0xa5uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0xdduy; 0x37uy; 0xbcuy; 0x9fuy; 0x0buy; 0x3auy; 0x47uy; 0x88uy; 0xf9uy; 0xb5uy; 0x49uy;
          0x66uy; 0xf2uy; 0x52uy; 0x17uy; 0x4cuy; 0x8cuy; 0xe4uy; 0x87uy; 0xcbuy; 0xe5uy; 0x9cuy;
          0x53uy; 0xc2uy; 0x2buy; 0x81uy; 0xbfuy; 0x77uy; 0x62uy; 0x1auy; 0x7cuy; 0xe7uy; 0x61uy;
          0x6duy; 0xcbuy; 0x5buy; 0x1euy; 0x2euy; 0xe6uy; 0x3cuy; 0x2cuy; 0x30uy; 0x9buy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xa0uy; 0xcfuy; 0x03uy; 0xf7uy; 0xbauy; 0xdduy; 0x0cuy; 0x3cuy; 0x3cuy; 0x4euy; 0xa3uy;
          0x71uy; 0x7fuy; 0x5auy; 0x4fuy; 0xb7uy; 0xe6uy; 0x7buy; 0x2euy; 0x56uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x5fuy; 0x48uy; 0x5cuy; 0x63uy; 0x7auy; 0xe3uy; 0x0buy; 0x1euy; 0x30uy; 0x49uy; 0x7fuy;
          0x0fuy; 0xb7uy; 0xecuy; 0x36uy; 0x4euy; 0x13uy; 0xc9uy; 0x06uy; 0xe2uy; 0x81uy; 0x3duy;
          0xaauy; 0x34uy; 0x16uy; 0x1buy; 0x7auy; 0xc4uy; 0xa4uy; 0xfduy; 0x7auy; 0x1buy; 0xdduy;
          0xd7uy; 0x96uy; 0x01uy; 0xbbuy; 0xd2uy; 0x2cuy; 0xefuy; 0x1fuy; 0x57uy; 0xcbuy; 0xc7uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xa5uy; 0x44uy; 0xe0uy; 0x6fuy; 0x1auy; 0x07uy; 0xceuy; 0xb1uy; 0x75uy; 0xa5uy; 0x1duy;
          0x6duy; 0x9cuy; 0x01uy; 0x11uy; 0xb3uy; 0xe1uy; 0x5euy; 0x98uy; 0x59uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0xf6uy; 0xc2uy; 0x37uy; 0xfbuy; 0x3cuy; 0xfeuy; 0x95uy; 0xecuy; 0x84uy; 0x14uy; 0xccuy;
          0x16uy; 0xd2uy; 0x03uy; 0xb4uy; 0x87uy; 0x4euy; 0x64uy; 0x4cuy; 0xc9uy; 0xa5uy; 0x43uy;
          0x46uy; 0x5cuy; 0xaduy; 0x2duy; 0xc5uy; 0x63uy; 0x48uy; 0x8auy; 0x65uy; 0x9euy; 0x8auy;
          0x2euy; 0x7cuy; 0x98uy; 0x1euy; 0x2auy; 0x9fuy; 0x22uy; 0xe5uy; 0xe8uy; 0x68uy; 0xffuy;
          0xe1uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x19uy; 0x9duy; 0x98uy; 0x6euy; 0xd9uy; 0x91uy; 0xb9uy; 0x9auy; 0x07uy; 0x1fuy; 0x45uy;
          0x0cuy; 0x6buy; 0x11uy; 0x21uy; 0xa7uy; 0x27uy; 0xe8uy; 0xc7uy; 0x35uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0xdauy; 0x7auy; 0xb3uy; 0x29uy; 0x15uy; 0x53uy; 0xc6uy; 0x59uy; 0x87uy; 0x3cuy; 0x95uy;
          0x91uy; 0x37uy; 0x68uy; 0x95uy; 0x3cuy; 0x6euy; 0x52uy; 0x6duy; 0x3auy; 0x26uy; 0x59uy;
          0x08uy; 0x98uy; 0xc0uy; 0xaduy; 0xe8uy; 0x9fuy; 0xf5uy; 0x6fuy; 0xbduy; 0x11uy; 0x0fuy;
          0x14uy; 0x36uy; 0xafuy; 0x59uy; 0x0buy; 0x17uy; 0xfeuy; 0xd4uy; 0x9fuy; 0x8cuy; 0x4buy;
          0x2buy; 0x1euy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x33uy; 0xbauy; 0xc6uy; 0x10uy; 0x4buy; 0x0auy; 0xd6uy; 0x12uy; 0x8duy; 0x09uy; 0x1buy;
          0x5duy; 0x5euy; 0x29uy; 0x99uy; 0x09uy; 0x9cuy; 0x9fuy; 0x05uy; 0xdeuy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x8cuy; 0xfauy; 0x5fuy; 0xd5uy; 0x6euy; 0xe2uy; 0x39uy; 0xcauy; 0x47uy; 0x73uy; 0x75uy;
          0x91uy; 0xcbuy; 0xa1uy; 0x03uy; 0xe4uy; 0x1auy; 0x18uy; 0xacuy; 0xf8uy; 0xe8uy; 0xd2uy;
          0x57uy; 0xb0uy; 0xdbuy; 0xe8uy; 0x85uy; 0x11uy; 0x34uy; 0xa8uy; 0x1fuy; 0xf6uy; 0xb2uy;
          0xe9uy; 0x71uy; 0x04uy; 0xb3uy; 0x9buy; 0x76uy; 0xe1uy; 0x9duy; 0xa2uy; 0x56uy; 0xa1uy;
          0x7cuy; 0xe5uy; 0x2duy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x76uy; 0xd7uy; 0xdbuy; 0x6euy; 0x18uy; 0xc1uy; 0xf4uy; 0xaeuy; 0x22uy; 0x5cuy; 0xe8uy;
          0xccuy; 0xc9uy; 0x3cuy; 0x8fuy; 0x9auy; 0x0duy; 0xfeuy; 0xb9uy; 0x69uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x57uy; 0xe8uy; 0x96uy; 0x59uy; 0xd8uy; 0x78uy; 0xf3uy; 0x60uy; 0xafuy; 0x6duy; 0xe4uy;
          0x5auy; 0x9auy; 0x5euy; 0x37uy; 0x2euy; 0xf4uy; 0x0cuy; 0x38uy; 0x49uy; 0x88uy; 0xe8uy;
          0x26uy; 0x40uy; 0xa3uy; 0xd5uy; 0xe4uy; 0xb7uy; 0x6duy; 0x2euy; 0xf1uy; 0x81uy; 0x78uy;
          0x0buy; 0x9auy; 0x09uy; 0x9auy; 0xc0uy; 0x6euy; 0xf0uy; 0xf8uy; 0xa7uy; 0xf3uy; 0xf7uy;
          0x64uy; 0x20uy; 0x97uy; 0x20uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xf6uy; 0x52uy; 0xf3uy; 0xb1uy; 0x54uy; 0x9fuy; 0x16uy; 0x71uy; 0x0cuy; 0x74uy; 0x02uy;
          0x89uy; 0x59uy; 0x11uy; 0xe2uy; 0xb8uy; 0x6auy; 0x9buy; 0x2auy; 0xeeuy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0xb9uy; 0x1euy; 0x64uy; 0x23uy; 0x5duy; 0xbduy; 0x23uy; 0x4euy; 0xeauy; 0x2auy; 0xe1uy;
          0x4auy; 0x92uy; 0xa1uy; 0x73uy; 0xebuy; 0xe8uy; 0x35uy; 0x34uy; 0x72uy; 0x39uy; 0xcfuy;
          0xf8uy; 0xb0uy; 0x20uy; 0x74uy; 0x41uy; 0x6fuy; 0x55uy; 0xc6uy; 0xb6uy; 0x0duy; 0xc6uy;
          0xceuy; 0xd0uy; 0x6auy; 0xe9uy; 0xf8uy; 0xd7uy; 0x05uy; 0x50uy; 0x5fuy; 0x0duy; 0x61uy;
          0x7euy; 0x4buy; 0x29uy; 0xaeuy; 0xf9uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x63uy; 0xfauy; 0xebuy; 0xb8uy; 0x07uy; 0xf3uy; 0x2buy; 0xe7uy; 0x08uy; 0xcfuy; 0x00uy;
          0xfcuy; 0x35uy; 0x51uy; 0x99uy; 0x91uy; 0xdcuy; 0x4euy; 0x7fuy; 0x68uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0xe4uy; 0x2auy; 0x67uy; 0x36uy; 0x2auy; 0x58uy; 0x1euy; 0x8cuy; 0xf3uy; 0xd8uy; 0x47uy;
          0x50uy; 0x22uy; 0x15uy; 0x75uy; 0x5duy; 0x7auy; 0xd4uy; 0x25uy; 0xcauy; 0x03uy; 0x0cuy;
          0x43uy; 0x60uy; 0xb0uy; 0xf7uy; 0xefuy; 0x51uy; 0x3euy; 0x69uy; 0x80uy; 0x26uy; 0x5fuy;
          0x61uy; 0xc9uy; 0xfauy; 0x18uy; 0xdduy; 0x9cuy; 0xe6uy; 0x68uy; 0xf3uy; 0x8duy; 0xbcuy;
          0x2auy; 0x1euy; 0xf8uy; 0xf8uy; 0x3cuy; 0xd6uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x0euy; 0x67uy; 0x30uy; 0xbcuy; 0x4auy; 0x0euy; 0x93uy; 0x22uy; 0xeauy; 0x20uy; 0x5fuy;
          0x4euy; 0xdfuy; 0xffuy; 0x1fuy; 0xffuy; 0xdauy; 0x26uy; 0xafuy; 0x0auy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x63uy; 0x4duy; 0xb9uy; 0x2cuy; 0x22uy; 0x01uy; 0x0euy; 0x1cuy; 0xbfuy; 0x1euy; 0x16uy;
          0x23uy; 0x92uy; 0x31uy; 0x80uy; 0x40uy; 0x6cuy; 0x51uy; 0x52uy; 0x72uy; 0x20uy; 0x9auy;
          0x8auy; 0xccuy; 0x42uy; 0xdeuy; 0x05uy; 0xccuy; 0x2euy; 0x96uy; 0xa1uy; 0xe9uy; 0x4cuy;
          0x1fuy; 0x9fuy; 0x6buy; 0x93uy; 0x23uy; 0x4buy; 0x7fuy; 0x4cuy; 0x55uy; 0xdeuy; 0x8buy;
          0x19uy; 0x61uy; 0xa3uy; 0xbfuy; 0x35uy; 0x22uy; 0x59uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xb6uy; 0x1auy; 0x3auy; 0x6fuy; 0x42uy; 0xe8uy; 0xe6uy; 0x60uy; 0x4buy; 0x93uy; 0x19uy;
          0x6cuy; 0x43uy; 0xc9uy; 0xe8uy; 0x4duy; 0x53uy; 0x59uy; 0xe6uy; 0xfeuy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0xccuy; 0x6cuy; 0xa3uy; 0xa8uy; 0xcbuy; 0x39uy; 0x1cuy; 0xd8uy; 0xa5uy; 0xafuy; 0xf1uy;
          0xfauy; 0xa7uy; 0xb3uy; 0xffuy; 0xbduy; 0xd2uy; 0x1auy; 0x5auy; 0x3cuy; 0xe6uy; 0x6cuy;
          0xfauy; 0xdduy; 0xbfuy; 0xe8uy; 0xb1uy; 0x79uy; 0xe4uy; 0xc8uy; 0x60uy; 0xbeuy; 0x5euy;
          0xc6uy; 0x6buy; 0xd2uy; 0xc6uy; 0xdeuy; 0x6auy; 0x39uy; 0xa2uy; 0x56uy; 0x22uy; 0xf9uy;
          0xf2uy; 0xfcuy; 0xb3uy; 0xfcuy; 0x05uy; 0xafuy; 0x12uy; 0xb5uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x32uy; 0xd9uy; 0x79uy; 0xcauy; 0x1buy; 0x3euy; 0xd0uy; 0xeduy; 0x8cuy; 0x89uy; 0x0duy;
          0x99uy; 0xecuy; 0x6duy; 0xd8uy; 0x5euy; 0x6cuy; 0x16uy; 0xabuy; 0xf4uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x7cuy; 0x0euy; 0x6auy; 0x0duy; 0x35uy; 0xf8uy; 0xacuy; 0x85uy; 0x4cuy; 0x72uy; 0x45uy;
          0xebuy; 0xc7uy; 0x36uy; 0x93uy; 0x73uy; 0x1buy; 0xbbuy; 0xc3uy; 0xe6uy; 0xfauy; 0xb6uy;
          0x44uy; 0x46uy; 0x6duy; 0xe2uy; 0x7buy; 0xb5uy; 0x22uy; 0xfcuy; 0xb9uy; 0x93uy; 0x07uy;
          0x12uy; 0x6auy; 0xe7uy; 0x18uy; 0xfeuy; 0x8fuy; 0x00uy; 0x74uy; 0x2euy; 0x6euy; 0x5cuy;
          0xb7uy; 0xa6uy; 0x87uy; 0xc8uy; 0x84uy; 0x47uy; 0xcbuy; 0xc9uy; 0x61uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x6fuy; 0x18uy; 0x19uy; 0x0buy; 0xd2uy; 0xd0uy; 0x2fuy; 0xc9uy; 0x3buy; 0xceuy; 0x64uy;
          0x75uy; 0x65uy; 0x75uy; 0xceuy; 0xa3uy; 0x6duy; 0x08uy; 0xb1uy; 0xc3uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0xc5uy; 0x58uy; 0x1duy; 0x40uy; 0xb3uy; 0x31uy; 0xe2uy; 0x40uy; 0x03uy; 0x90uy; 0x1buy;
          0xd6uy; 0xbfuy; 0x24uy; 0x4auy; 0xcauy; 0x9euy; 0x96uy; 0x01uy; 0xb9uy; 0xd8uy; 0x12uy;
          0x52uy; 0xbbuy; 0x38uy; 0x04uy; 0x86uy; 0x42uy; 0x73uy; 0x1fuy; 0x11uy; 0x46uy; 0xb8uy;
          0xa4uy; 0xc6uy; 0x9fuy; 0x88uy; 0xe1uy; 0x48uy; 0xb2uy; 0xc8uy; 0xf8uy; 0xc1uy; 0x4fuy;
          0x15uy; 0xe1uy; 0xd6uy; 0xdauy; 0x57uy; 0xb2uy; 0xdauy; 0xa9uy; 0x99uy; 0x1euy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x68uy; 0xf5uy; 0x25uy; 0xfeuy; 0xeauy; 0x1duy; 0x8duy; 0xbeuy; 0x01uy; 0x17uy; 0xe4uy;
          0x17uy; 0xcauy; 0x46uy; 0x70uy; 0x8duy; 0x18uy; 0xd7uy; 0x62uy; 0x9auy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0xecuy; 0x6buy; 0x4auy; 0x88uy; 0x71uy; 0x3duy; 0xf2uy; 0x7cuy; 0x0fuy; 0x2duy; 0x02uy;
          0xe7uy; 0x38uy; 0xb6uy; 0x9duy; 0xb4uy; 0x3auy; 0xbduy; 0xa3uy; 0x92uy; 0x13uy; 0x17uy;
          0x25uy; 0x9cuy; 0x86uy; 0x4cuy; 0x1cuy; 0x38uy; 0x6euy; 0x9auy; 0x5auy; 0x3fuy; 0x53uy;
          0x3duy; 0xc0uy; 0x5fuy; 0x3buy; 0xeeuy; 0xb2uy; 0xbeuy; 0xc2uy; 0xaauy; 0xc8uy; 0xe0uy;
          0x6duy; 0xb4uy; 0xc6uy; 0xcbuy; 0x3cuy; 0xdduy; 0xcfuy; 0x69uy; 0x7euy; 0x03uy; 0xd5uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xa7uy; 0x27uy; 0x2euy; 0x23uy; 0x08uy; 0x62uy; 0x2fuy; 0xf7uy; 0xa3uy; 0x39uy; 0x46uy;
          0x0auy; 0xdcuy; 0x61uy; 0xefuy; 0xd0uy; 0xeauy; 0x8duy; 0xabuy; 0xdcuy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x03uy; 0x21uy; 0x73uy; 0x6buy; 0xebuy; 0xa5uy; 0x78uy; 0xe9uy; 0x0auy; 0xbcuy; 0x1auy;
          0x90uy; 0xaauy; 0x56uy; 0x15uy; 0x7duy; 0x87uy; 0x16uy; 0x18uy; 0xf6uy; 0xdeuy; 0x0duy;
          0x76uy; 0x4cuy; 0xc8uy; 0xc9uy; 0x1euy; 0x06uy; 0xc6uy; 0x8euy; 0xcduy; 0x3buy; 0x9duy;
          0xe3uy; 0x82uy; 0x40uy; 0x64uy; 0x50uy; 0x33uy; 0x84uy; 0xdbuy; 0x67uy; 0xbeuy; 0xb7uy;
          0xfeuy; 0x01uy; 0x22uy; 0x32uy; 0xdauy; 0xcauy; 0xefuy; 0x93uy; 0xa0uy; 0x00uy; 0xfbuy;
          0xa7uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xaeuy; 0xf8uy; 0x43uy; 0xb8uy; 0x69uy; 0x16uy; 0xc1uy; 0x6fuy; 0x66uy; 0xc8uy; 0x4duy;
          0x83uy; 0xa6uy; 0x00uy; 0x5duy; 0x23uy; 0xfduy; 0x00uy; 0x5cuy; 0x9euy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0xd0uy; 0xa2uy; 0x49uy; 0xa9uy; 0x7buy; 0x5fuy; 0x14uy; 0x86uy; 0x72uy; 0x1auy; 0x50uy;
          0xd4uy; 0xc4uy; 0xabuy; 0x3fuy; 0x5duy; 0x67uy; 0x4auy; 0x0euy; 0x29uy; 0x92uy; 0x5duy;
          0x5buy; 0xf2uy; 0x67uy; 0x8euy; 0xf6uy; 0xd8uy; 0xd5uy; 0x21uy; 0xe4uy; 0x56uy; 0xbduy;
          0x84uy; 0xaauy; 0x75uy; 0x53uy; 0x28uy; 0xc8uy; 0x3fuy; 0xc8uy; 0x90uy; 0x83uy; 0x77uy;
          0x26uy; 0xa8uy; 0xe7uy; 0x87uy; 0x7buy; 0x57uy; 0x0duy; 0xbauy; 0x39uy; 0x57uy; 0x9auy;
          0xabuy; 0xdduy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xbeuy; 0x2cuy; 0xd6uy; 0xf3uy; 0x80uy; 0x96uy; 0x9buy; 0xe5uy; 0x9cuy; 0xdeuy; 0x2duy;
          0xffuy; 0x5euy; 0x84uy; 0x8auy; 0x44uy; 0xe7uy; 0x88uy; 0x0buy; 0xd6uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0xc3uy; 0x21uy; 0x38uy; 0x53uy; 0x11uy; 0x18uy; 0xf0uy; 0x8cuy; 0x7duy; 0xccuy; 0x29uy;
          0x24uy; 0x28uy; 0xaduy; 0x20uy; 0xb4uy; 0x5auy; 0xb2uy; 0x7duy; 0x95uy; 0x17uy; 0xa1uy;
          0x84uy; 0x45uy; 0xf3uy; 0x8buy; 0x8fuy; 0x0cuy; 0x27uy; 0x95uy; 0xbcuy; 0xdfuy; 0xe3uy;
          0xffuy; 0xe3uy; 0x84uy; 0xe6uy; 0x5euy; 0xcbuy; 0xf7uy; 0x4duy; 0x2cuy; 0x9duy; 0x0duy;
          0xa8uy; 0x83uy; 0x98uy; 0x57uy; 0x53uy; 0x26uy; 0x07uy; 0x49uy; 0x04uy; 0xc1uy; 0x70uy;
          0x9buy; 0xa0uy; 0x72uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xe5uy; 0xebuy; 0x45uy; 0x43uy; 0xdeuy; 0xeeuy; 0x8fuy; 0x6auy; 0x52uy; 0x87uy; 0x84uy;
          0x5auy; 0xf8uy; 0xb5uy; 0x93uy; 0xa9uy; 0x5auy; 0x97uy; 0x49uy; 0xa1uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0xb0uy; 0xf4uy; 0xcfuy; 0xb9uy; 0x39uy; 0xeauy; 0x78uy; 0x5euy; 0xabuy; 0xb7uy; 0xe7uy;
          0xcauy; 0x7cuy; 0x47uy; 0x6cuy; 0xdduy; 0x9buy; 0x22uy; 0x7fuy; 0x01uy; 0x5duy; 0x90uy;
          0x53uy; 0x68uy; 0xbauy; 0x00uy; 0xaeuy; 0x96uy; 0xb9uy; 0xaauy; 0xf7uy; 0x20uy; 0x29uy;
          0x74uy; 0x91uy; 0xb3uy; 0x92uy; 0x12uy; 0x67uy; 0x57uy; 0x6buy; 0x72uy; 0xc8uy; 0xf5uy;
          0x8duy; 0x57uy; 0x76uy; 0x17uy; 0xe8uy; 0x44uy; 0xf9uy; 0xf0uy; 0x75uy; 0x9buy; 0x39uy;
          0x9cuy; 0x6buy; 0x06uy; 0x4cuy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x53uy; 0x4cuy; 0x85uy; 0x04uy; 0x48uy; 0xdduy; 0x48uy; 0x67uy; 0x87uy; 0xb6uy; 0x2buy;
          0xdeuy; 0xc2uy; 0xd4uy; 0xa0uy; 0xb1uy; 0x40uy; 0xa1uy; 0xb1uy; 0x70uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0xbduy; 0x02uy; 0xe5uy; 0x1buy; 0x0cuy; 0xf2uy; 0xc2uy; 0xb8uy; 0xd2uy; 0x04uy; 0xa0uy;
          0x26uy; 0xb4uy; 0x1auy; 0x66uy; 0xfbuy; 0xfcuy; 0x2auy; 0xc3uy; 0x7euy; 0xe9uy; 0x41uy;
          0x1fuy; 0xc4uy; 0x49uy; 0xc8uy; 0xd1uy; 0x19uy; 0x4auy; 0x07uy; 0x92uy; 0xa2uy; 0x8euy;
          0xe7uy; 0x31uy; 0x40uy; 0x7duy; 0xfcuy; 0x89uy; 0xb6uy; 0xdfuy; 0xc2uy; 0xb1uy; 0x0fuy;
          0xaauy; 0x27uy; 0x72uy; 0x3auy; 0x18uy; 0x4auy; 0xfeuy; 0xf8uy; 0xfduy; 0x83uy; 0xdeuy;
          0xf8uy; 0x58uy; 0xa3uy; 0x2duy; 0x3fuy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x6fuy; 0xbfuy; 0xa6uy; 0xe4uy; 0xeduy; 0xceuy; 0x4cuy; 0xc8uy; 0x5auy; 0x84uy; 0x5buy;
          0xf0uy; 0xd2uy; 0x28uy; 0xdcuy; 0x39uy; 0xacuy; 0xefuy; 0xc2uy; 0xfauy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0xe3uy; 0x31uy; 0x46uy; 0xb8uy; 0x3euy; 0x4buy; 0xb6uy; 0x71uy; 0x39uy; 0x22uy; 0x18uy;
          0xdauy; 0x9auy; 0x77uy; 0xf8uy; 0xd9uy; 0xf5uy; 0x97uy; 0x41uy; 0x47uy; 0x18uy; 0x2fuy;
          0xb9uy; 0x5buy; 0xa6uy; 0x62uy; 0xcbuy; 0x66uy; 0x01uy; 0x19uy; 0x89uy; 0xc1uy; 0x6duy;
          0x9auy; 0xf1uy; 0x04uy; 0x73uy; 0x5duy; 0x6fuy; 0x79uy; 0x84uy; 0x1auy; 0xa4uy; 0xd1uy;
          0xdfuy; 0x27uy; 0x66uy; 0x15uy; 0xb5uy; 0x01uy; 0x08uy; 0xdfuy; 0x8auy; 0x29uy; 0xdbuy;
          0xc9uy; 0xdeuy; 0x31uy; 0xf4uy; 0x26uy; 0x0duy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x01uy; 0x88uy; 0x72uy; 0x69uy; 0x1duy; 0x9buy; 0x04uy; 0xe8uy; 0x22uy; 0x0euy; 0x09uy;
          0x18uy; 0x7duy; 0xf5uy; 0xbcuy; 0x5fuy; 0xa6uy; 0x25uy; 0x7cuy; 0xd9uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x41uy; 0x1cuy; 0x13uy; 0xc7uy; 0x50uy; 0x73uy; 0xc1uy; 0xe2uy; 0xd4uy; 0xb1uy; 0xecuy;
          0xf1uy; 0x31uy; 0x39uy; 0xbauy; 0x96uy; 0x56uy; 0xcduy; 0x35uy; 0xc1uy; 0x42uy; 0x01uy;
          0xf1uy; 0xc7uy; 0xc6uy; 0xf0uy; 0xeeuy; 0xb5uy; 0x8duy; 0x2duy; 0xbfuy; 0xe3uy; 0x5buy;
          0xfduy; 0xecuy; 0xccuy; 0x92uy; 0xc3uy; 0x96uy; 0x1cuy; 0xfauy; 0xbbuy; 0x59uy; 0x0buy;
          0xc1uy; 0xebuy; 0x77uy; 0xeauy; 0xc1uy; 0x57uy; 0x32uy; 0xfbuy; 0x02uy; 0x75uy; 0x79uy;
          0x86uy; 0x80uy; 0xe0uy; 0xc7uy; 0x29uy; 0x2euy; 0x50uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xd9uy; 0x8duy; 0x51uy; 0x2auy; 0x35uy; 0x57uy; 0x2fuy; 0x8buy; 0xd2uy; 0x0duy; 0xe6uy;
          0x2euy; 0x95uy; 0x10uy; 0xccuy; 0x21uy; 0x14uy; 0x5cuy; 0x5buy; 0xf4uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0xf2uy; 0xc7uy; 0x6euy; 0xf6uy; 0x17uy; 0xfauy; 0x2buy; 0xfcuy; 0x8auy; 0x4duy; 0x6buy;
          0xcbuy; 0xb1uy; 0x5fuy; 0xe8uy; 0x84uy; 0x36uy; 0xfduy; 0xc2uy; 0x16uy; 0x5duy; 0x30uy;
          0x74uy; 0x62uy; 0x95uy; 0x79uy; 0x07uy; 0x9duy; 0x4duy; 0x5buy; 0x86uy; 0xf5uy; 0x08uy;
          0x1auy; 0xb1uy; 0x77uy; 0xb4uy; 0xc3uy; 0xf5uy; 0x30uy; 0x37uy; 0x6cuy; 0x9cuy; 0x92uy;
          0x4cuy; 0xbduy; 0x42uy; 0x1auy; 0x8duy; 0xafuy; 0x88uy; 0x30uy; 0xd0uy; 0x94uy; 0x0cuy;
          0x4fuy; 0xb7uy; 0x58uy; 0x98uy; 0x65uy; 0x83uy; 0x06uy; 0x99uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x9fuy; 0x3euy; 0xa2uy; 0x55uy; 0xf6uy; 0xafuy; 0x95uy; 0xc5uy; 0x45uy; 0x4euy; 0x55uy;
          0xd7uy; 0x35uy; 0x4cuy; 0xabuy; 0xb4uy; 0x53uy; 0x52uy; 0xeauy; 0x0buy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x45uy; 0x92uy; 0x7euy; 0x32uy; 0xdduy; 0xf8uy; 0x01uy; 0xcauy; 0xf3uy; 0x5euy; 0x18uy;
          0xe7uy; 0xb5uy; 0x07uy; 0x8buy; 0x7fuy; 0x54uy; 0x35uy; 0x27uy; 0x82uy; 0x12uy; 0xecuy;
          0x6buy; 0xb9uy; 0x9duy; 0xf8uy; 0x84uy; 0xf4uy; 0x9buy; 0x32uy; 0x7cuy; 0x64uy; 0x86uy;
          0xfeuy; 0xaeuy; 0x46uy; 0xbauy; 0x18uy; 0x7duy; 0xc1uy; 0xccuy; 0x91uy; 0x45uy; 0x12uy;
          0x1euy; 0x14uy; 0x92uy; 0xe6uy; 0xb0uy; 0x6euy; 0x90uy; 0x07uy; 0x39uy; 0x4duy; 0xc3uy;
          0x3buy; 0x77uy; 0x48uy; 0xf8uy; 0x6auy; 0xc3uy; 0x20uy; 0x7cuy; 0xfeuy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xa7uy; 0x0cuy; 0xfbuy; 0xfeuy; 0x75uy; 0x63uy; 0xdduy; 0x0euy; 0x66uy; 0x5cuy; 0x7cuy;
          0x67uy; 0x15uy; 0xa9uy; 0x6auy; 0x8duy; 0x75uy; 0x69uy; 0x50uy; 0xc0uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x7cuy; 0x9cuy; 0x67uy; 0x32uy; 0x3auy; 0x1duy; 0xf1uy; 0xaduy; 0xbfuy; 0xe5uy; 0xceuy;
          0xb4uy; 0x15uy; 0xeauy; 0xefuy; 0x01uy; 0x55uy; 0xecuy; 0xe2uy; 0x82uy; 0x0fuy; 0x4duy;
          0x50uy; 0xc1uy; 0xecuy; 0x22uy; 0xcbuy; 0xa4uy; 0x92uy; 0x8auy; 0xc6uy; 0x56uy; 0xc8uy;
          0x3fuy; 0xe5uy; 0x85uy; 0xdbuy; 0x6auy; 0x78uy; 0xceuy; 0x40uy; 0xbcuy; 0x42uy; 0x75uy;
          0x7auy; 0xbauy; 0x7euy; 0x5auy; 0x3fuy; 0x58uy; 0x24uy; 0x28uy; 0xd6uy; 0xcauy; 0x68uy;
          0xd0uy; 0xc3uy; 0x97uy; 0x83uy; 0x36uy; 0xa6uy; 0xefuy; 0xb7uy; 0x29uy; 0x61uy; 0x3euy;
          0x8duy; 0x99uy; 0x79uy; 0x01uy; 0x62uy; 0x04uy; 0xbfuy; 0xd9uy; 0x21uy; 0x32uy; 0x2fuy;
          0xdduy; 0x52uy; 0x22uy; 0x18uy; 0x35uy; 0x54uy; 0x44uy; 0x7duy; 0xe5uy; 0xe6uy; 0xe9uy;
          0xbbuy; 0xe6uy; 0xeduy; 0xf7uy; 0x6duy; 0x7buy; 0x71uy; 0xe1uy; 0x8duy; 0xc2uy; 0xe8uy;
          0xd6uy; 0xdcuy; 0x89uy; 0xb7uy; 0x39uy; 0x83uy; 0x64uy; 0xf6uy; 0x52uy; 0xfauy; 0xfcuy;
          0x73uy; 0x43uy; 0x29uy; 0xaauy; 0xfauy; 0x3duy; 0xcduy; 0x45uy; 0xd4uy; 0xf3uy; 0x1euy;
          0x38uy; 0x8euy; 0x4fuy; 0xafuy; 0xd7uy; 0xfcuy; 0x64uy; 0x95uy; 0xf3uy; 0x7cuy; 0xa5uy;
          0xcbuy; 0xabuy; 0x7fuy; 0x54uy; 0xd5uy; 0x86uy; 0x46uy; 0x3duy; 0xa4uy; 0xbfuy; 0xeauy;
          0xa3uy; 0xbauy; 0xe0uy; 0x9fuy; 0x7buy; 0x8euy; 0x92uy; 0x39uy; 0xd8uy; 0x32uy; 0xb4uy;
          0xf0uy; 0xa7uy; 0x33uy; 0xaauy; 0x60uy; 0x9cuy; 0xc1uy; 0xf8uy; 0xd4uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xd8uy; 0xfduy; 0x6auy; 0x91uy; 0xefuy; 0x3buy; 0x6cuy; 0xeduy; 0x05uy; 0xb9uy; 0x83uy;
          0x58uy; 0xa9uy; 0x91uy; 0x07uy; 0xc1uy; 0xfauy; 0xc8uy; 0xc8uy; 0x07uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x6cuy; 0xb7uy; 0x0duy; 0x19uy; 0xc0uy; 0x96uy; 0x20uy; 0x0fuy; 0x92uy; 0x49uy; 0xd2uy;
          0xdbuy; 0xc0uy; 0x42uy; 0x99uy; 0xb0uy; 0x08uy; 0x5euy; 0xb0uy; 0x68uy; 0x25uy; 0x75uy;
          0x60uy; 0xbeuy; 0x3auy; 0x30uy; 0x7duy; 0xbduy; 0x74uy; 0x1auy; 0x33uy; 0x78uy; 0xebuy;
          0xfauy; 0x03uy; 0xfcuy; 0xcauy; 0x61uy; 0x08uy; 0x83uy; 0xb0uy; 0x7fuy; 0x7fuy; 0xeauy;
          0x56uy; 0x3auy; 0x86uy; 0x65uy; 0x71uy; 0x82uy; 0x24uy; 0x72uy; 0xdauy; 0xdeuy; 0x8auy;
          0x0buy; 0xecuy; 0x4buy; 0x98uy; 0x20uy; 0x2duy; 0x47uy; 0xa3uy; 0x44uy; 0x31uy; 0x29uy;
          0x76uy; 0xa7uy; 0xbcuy; 0xb3uy; 0x96uy; 0x44uy; 0x27uy; 0xeauy; 0xcbuy; 0x5buy; 0x05uy;
          0x25uy; 0xdbuy; 0x22uy; 0x06uy; 0x65uy; 0x99uy; 0xb8uy; 0x1buy; 0xe4uy; 0x1euy; 0x5auy;
          0xdauy; 0xf1uy; 0x57uy; 0xd9uy; 0x25uy; 0xfauy; 0xc0uy; 0x4buy; 0x06uy; 0xebuy; 0x6euy;
          0x01uy; 0xdeuy; 0xb7uy; 0x53uy; 0xbauy; 0xbfuy; 0x33uy; 0xbeuy; 0x16uy; 0x16uy; 0x2buy;
          0x21uy; 0x4euy; 0x8duy; 0xb0uy; 0x17uy; 0x21uy; 0x2fuy; 0xafuy; 0xa5uy; 0x12uy; 0xcduy;
          0xc8uy; 0xc0uy; 0xd0uy; 0xa1uy; 0x5cuy; 0x10uy; 0xf6uy; 0x32uy; 0xe8uy; 0xf4uy; 0xf4uy;
          0x77uy; 0x92uy; 0xc6uy; 0x4duy; 0x3fuy; 0x02uy; 0x60uy; 0x04uy; 0xd1uy; 0x73uy; 0xdfuy;
          0x50uy; 0xcfuy; 0x0auy; 0xa7uy; 0x97uy; 0x60uy; 0x66uy; 0xa7uy; 0x9auy; 0x8duy; 0x78uy;
          0xdeuy; 0xeeuy; 0xecuy; 0x95uy; 0x1duy; 0xabuy; 0x7cuy; 0xc9uy; 0x0fuy; 0x68uy; 0xd1uy;
          0x6fuy; 0x78uy; 0x66uy; 0x71uy; 0xfeuy; 0xbauy; 0x0buy; 0x7duy; 0x26uy; 0x9duy; 0x92uy;
          0x94uy; 0x1cuy; 0x4fuy; 0x02uy; 0xf4uy; 0x32uy; 0xaauy; 0x5cuy; 0xe2uy; 0xaauy; 0xb6uy;
          0x19uy; 0x4duy; 0xccuy; 0x6fuy; 0xd3uy; 0xaeuy; 0x36uy; 0xc8uy; 0x43uy; 0x32uy; 0x74uy;
          0xefuy; 0x6buy; 0x1buy; 0xd0uy; 0xd3uy; 0x14uy; 0x63uy; 0x6buy; 0xe4uy; 0x7buy; 0xa3uy;
          0x8duy; 0x19uy; 0x48uy; 0x34uy; 0x3auy; 0x38uy; 0xbfuy; 0x94uy; 0x06uy; 0x52uy; 0x3auy;
          0x0buy; 0x2auy; 0x8cuy; 0xd7uy; 0x8euy; 0xd6uy; 0x26uy; 0x6euy; 0xe3uy; 0xc9uy; 0xb5uy;
          0xc6uy; 0x06uy; 0x20uy; 0xb3uy; 0x08uy; 0xccuy; 0x6buy; 0x3auy; 0x73uy; 0xc6uy; 0x06uy;
          0x0duy; 0x52uy; 0x68uy; 0xa7uy; 0xd8uy; 0x2buy; 0x6auy; 0x33uy; 0xb9uy; 0x3auy; 0x6fuy;
          0xd6uy; 0xfeuy; 0x1duy; 0xe5uy; 0x52uy; 0x31uy; 0xd1uy; 0x2cuy; 0x97uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0x4auy; 0x75uy; 0xa4uy; 0x06uy; 0xf4uy; 0xdeuy; 0x5fuy; 0x9euy; 0x11uy; 0x32uy; 0x06uy;
          0x9duy; 0x66uy; 0x71uy; 0x7fuy; 0xc4uy; 0x24uy; 0x37uy; 0x63uy; 0x88uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0x64uy; 0x87uy; 0x97uy; 0x2duy; 0x88uy; 0xd0uy; 0xdduy; 0x39uy; 0x0duy; 0x8duy; 0x09uy;
          0xd1uy; 0x34uy; 0x86uy; 0x0fuy; 0x26uy; 0x3fuy; 0x88uy; 0xdfuy; 0x7auy; 0x34uy; 0x12uy;
          0x45uy; 0x7auy; 0xdfuy; 0x51uy; 0x0duy; 0xcfuy; 0x16uy; 0x4euy; 0x6cuy; 0xf0uy; 0x41uy;
          0x67uy; 0x9buy; 0x3auy; 0x19uy; 0xfcuy; 0xc5uy; 0x42uy; 0xafuy; 0x6auy; 0x23uy; 0x6auy;
          0xb0uy; 0x3duy; 0x66uy; 0xb2uy; 0xe8uy; 0xa1uy; 0x55uy; 0xd1uy; 0x06uy; 0x1auy; 0xb7uy;
          0x85uy; 0x9fuy; 0x75uy; 0x73uy; 0x27uy; 0x75uy; 0xffuy; 0xf6uy; 0x82uy; 0xf8uy; 0xf4uy;
          0xd5uy; 0xe5uy; 0x0duy; 0x3auy; 0xb3uy; 0x77uy; 0x0fuy; 0x4fuy; 0x66uy; 0xcbuy; 0x13uy;
          0x81uy; 0x55uy; 0xb4uy; 0x71uy; 0x5duy; 0x24uy; 0x5buy; 0x80uy; 0x69uy; 0x94uy; 0x8euy;
          0xa0uy; 0x16uy; 0xa4uy; 0x5buy; 0x7euy; 0xf0uy; 0xfduy; 0xdeuy; 0x93uy; 0x18uy; 0x8cuy;
          0x57uy; 0xeeuy; 0xf4uy; 0x71uy; 0x7fuy; 0x34uy; 0x25uy; 0x18uy; 0x1duy; 0xe5uy; 0xb9uy;
          0xa5uy; 0xd4uy; 0xe0uy; 0xa2uy; 0x96uy; 0x3fuy; 0x2auy; 0x67uy; 0xa3uy; 0x40uy; 0xebuy;
          0x1auy; 0xe9uy; 0x94uy; 0xb9uy; 0x8auy; 0x48uy; 0xabuy; 0x19uy; 0xb9uy; 0x0auy; 0xb7uy;
          0x43uy; 0x91uy; 0xc5uy; 0x04uy; 0x26uy; 0xd2uy; 0x82uy; 0x87uy; 0xacuy; 0x4fuy; 0x1euy;
          0xb9uy; 0x3fuy; 0x5auy; 0xf1uy; 0xa6uy; 0x8cuy; 0x7duy; 0xaeuy; 0x40uy; 0x87uy; 0x6buy;
          0x8auy; 0xfauy; 0xafuy; 0x35uy; 0xa1uy; 0x92uy; 0x93uy; 0xc1uy; 0x95uy; 0x2euy; 0x95uy;
          0x79uy; 0x78uy; 0xabuy; 0xeeuy; 0x40uy; 0xecuy; 0x32uy; 0xf2uy; 0xaauy; 0x88uy; 0x0cuy;
          0x95uy; 0x6cuy; 0x7euy; 0xb7uy; 0x2fuy; 0x11uy; 0x7buy; 0x39uy; 0x7cuy; 0xefuy; 0xcfuy;
          0xb4uy; 0xe7uy; 0x5auy; 0xceuy; 0x3buy; 0x08uy; 0x17uy; 0x76uy; 0xe4uy; 0x6buy; 0x13uy;
          0x52uy; 0x1euy; 0x93uy; 0x55uy; 0x9duy; 0x45uy; 0x3euy; 0x32uy; 0xabuy; 0x74uy; 0xebuy;
          0xc0uy; 0x85uy; 0x9buy; 0x9auy; 0x8duy; 0xd4uy; 0xd1uy; 0xd3uy; 0x90uy; 0x00uy; 0xebuy;
          0xe9uy; 0x5fuy; 0x98uy; 0x4duy; 0x80uy; 0xa3uy; 0xf5uy; 0x00uy; 0x4duy; 0xc9uy; 0x1auy;
          0x05uy; 0x1duy; 0xfbuy; 0xdfuy; 0xe9uy; 0x19uy; 0x4fuy; 0x4fuy; 0x9auy; 0x48uy; 0x3euy;
          0x4euy; 0x79uy; 0x55uy; 0x57uy; 0x7fuy; 0xb0uy; 0x93uy; 0x34uy; 0x64uy; 0xc6uy; 0x3euy;
          0xaeuy; 0xc7uy; 0x71uy; 0x04uy; 0x4duy; 0x59uy; 0xabuy; 0xc3uy; 0x02uy; 0x9auy; 0x07uy;
          0x95uy; 0x19uy; 0xf8uy; 0x46uy; 0x0auy; 0x69uy; 0x3buy; 0x25uy; 0xb4uy; 0xceuy; 0x20uy;
          0x7auy; 0xe9uy; 0xd9uy; 0x44uy; 0x7fuy; 0xc4uy; 0xc5uy; 0x44uy; 0x6euy; 0x6duy; 0xaduy;
          0x23uy; 0x4euy; 0x9auy; 0xfduy; 0xecuy; 0x0cuy; 0x56uy; 0x27uy; 0x98uy; 0xcduy; 0x02uy;
          0x97uy; 0x31uy; 0x83uy; 0x99uy; 0xe8uy; 0x38uy; 0xbeuy; 0x38uy; 0x58uy; 0x45uy; 0xc6uy;
          0xdduy; 0x79uy; 0xeduy; 0xe6uy; 0x6euy; 0x2auy; 0xe8uy; 0x0auy; 0xfeuy; 0xc6uy; 0x73uy;
          0x8duy; 0x4duy; 0x9buy; 0xf4uy; 0x4cuy; 0x8duy; 0x9euy; 0xdduy; 0xffuy; 0x6cuy; 0x5cuy;
          0xd2uy; 0xc9uy; 0x4euy; 0x34uy; 0x0euy; 0x0duy; 0xdauy; 0xc4uy; 0x03uy; 0x84uy; 0xb9uy;
          0xa1uy; 0x40uy; 0x8cuy; 0x9auy; 0x4buy; 0x98uy; 0xc3uy; 0x7auy; 0x60uy; 0x81uy; 0xd5uy;
          0x22uy; 0x0fuy; 0xbauy; 0x92uy; 0xf1uy; 0xd0uy; 0x31uy; 0x44uy; 0xdbuy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xa1uy; 0x35uy; 0xe3uy; 0x25uy; 0x81uy; 0xbbuy; 0x06uy; 0x28uy; 0x9buy; 0x8cuy; 0x83uy;
          0xf0uy; 0x40uy; 0xe9uy; 0x42uy; 0x1euy; 0xc7uy; 0x9buy; 0xbeuy; 0x01uy
        ]
      in
      Vec SHA1 plain cipher);
    (let plain: list FStar.UInt8.t =
        [
          0xbduy; 0x74uy; 0xe7uy; 0xf6uy; 0x07uy; 0xcduy; 0x7duy; 0x90uy; 0x5euy; 0x90uy; 0x17uy;
          0x5duy; 0x67uy; 0x65uy; 0x0auy; 0x6duy; 0xc2uy; 0xf8uy; 0xa4uy; 0xe2uy; 0xd4uy; 0xabuy;
          0x12uy; 0x49uy; 0xcauy; 0x88uy; 0x81uy; 0x2buy; 0xdauy; 0x79uy; 0x84uy; 0xdeuy; 0xccuy;
          0xbbuy; 0xb6uy; 0xa1uy; 0xbauy; 0x90uy; 0xa0uy; 0xe9uy; 0x14uy; 0x34uy; 0xdduy; 0xf5uy;
          0xe6uy; 0x13uy; 0x7buy; 0xa8uy; 0x5euy; 0x39uy; 0xa5uy; 0x98uy; 0x89uy; 0x0auy; 0x7fuy;
          0x63uy; 0x5duy; 0x33uy; 0x52uy; 0x42uy; 0xfcuy; 0xe0uy; 0xe9uy; 0xe0uy; 0x37uy; 0x30uy;
          0x3buy; 0x6cuy; 0x51uy; 0xe5uy; 0x4auy; 0xecuy; 0x06uy; 0x61uy; 0x4auy; 0xd5uy; 0xccuy;
          0xceuy; 0x06uy; 0xd9uy; 0x59uy; 0x9cuy; 0x80uy; 0x01uy; 0x65uy; 0x30uy; 0xd7uy; 0xfbuy;
          0xb1uy; 0xdauy; 0x6euy; 0xb5uy; 0x48uy; 0x08uy; 0x4buy; 0x2buy; 0x05uy; 0xbauy; 0xbduy;
          0x7duy; 0x55uy; 0x36uy; 0x42uy; 0x44uy; 0x3euy; 0xfduy; 0xa7uy; 0x26uy; 0xa1uy; 0xfduy;
          0x71uy; 0xa8uy; 0xbcuy; 0x08uy; 0x7cuy; 0x44uy; 0xf2uy; 0x85uy; 0xe2uy; 0xbcuy; 0xcfuy;
          0x66uy; 0x1euy; 0xaduy; 0x47uy; 0x5auy; 0x72uy; 0x67uy; 0x3euy; 0x43uy; 0x86uy; 0xfcuy;
          0x4euy; 0xeauy; 0x51uy; 0x97uy; 0xc4uy; 0xf1uy; 0x3cuy; 0x0fuy; 0xebuy; 0x0auy; 0x85uy;
          0xbcuy; 0x8euy; 0x67uy; 0xe2uy; 0x8auy; 0xb8uy; 0x72uy; 0x68uy; 0x4buy; 0xbeuy; 0xbduy;
          0xaauy; 0x52uy; 0x7fuy; 0x3cuy; 0x25uy; 0x3duy; 0xebuy; 0xb2uy; 0xdcuy; 0x12uy; 0xc2uy;
          0x69uy; 0x3fuy; 0x8euy; 0x9euy; 0x26uy; 0x51uy; 0xb9uy; 0x34uy; 0x5cuy; 0x0auy; 0xbeuy;
          0xd7uy; 0xa0uy; 0xfauy; 0xfauy; 0x3euy; 0x5duy; 0x30uy; 0x53uy; 0x86uy; 0xc9uy; 0x5auy;
          0xcbuy; 0x7auy; 0x17uy; 0x2euy; 0x54uy; 0x13uy; 0xefuy; 0x08uy; 0xe7uy; 0x3buy; 0x1buy;
          0xd4uy; 0xd0uy; 0xd6uy; 0x83uy; 0x2euy; 0x4cuy; 0x03uy; 0x5buy; 0xc8uy; 0x55uy; 0x9fuy;
          0x9buy; 0x0cuy; 0xbduy; 0x0cuy; 0xafuy; 0x03uy; 0x7auy; 0x30uy; 0x70uy; 0x76uy; 0x41uy;
          0xc0uy; 0x54uy; 0x53uy; 0x56uy; 0xbeuy; 0xe1uy; 0x51uy; 0xa2uy; 0x40uy; 0x68uy; 0xd7uy;
          0x06uy; 0x74uy; 0xefuy; 0x1buy; 0xefuy; 0xe1uy; 0x6fuy; 0x87uy; 0x2auy; 0xefuy; 0x40uy;
          0x60uy; 0xfauy; 0xaauy; 0xd1uy; 0xa9uy; 0x68uy; 0xc3uy; 0x9cuy; 0x45uy; 0xdbuy; 0xd7uy;
          0x59uy; 0x5duy; 0xe8uy; 0xf4uy; 0x72uy; 0x01uy; 0x6buy; 0x5auy; 0xb8uy; 0x12uy; 0xd7uy;
          0x7euy; 0x54uy; 0x5fuy; 0xcauy; 0x55uy; 0x00uy; 0x0euy; 0xe5uy; 0xceuy; 0x77uy; 0x3euy;
          0xdauy; 0xa1uy; 0x29uy; 0xeauy; 0xc6uy; 0x47uy; 0x34uy; 0x10uy; 0xc2uy; 0x49uy; 0x90uy;
          0x13uy; 0xb4uy; 0xbeuy; 0x89uy; 0x5fuy; 0x6cuy; 0x0fuy; 0x73uy; 0x4buy; 0xecuy; 0xfeuy;
          0x99uy; 0x43uy; 0x06uy; 0xe7uy; 0x76uy; 0x26uy; 0x2duy; 0x45uy; 0x28uy; 0xeduy; 0x85uy;
          0x77uy; 0x21uy; 0x8euy; 0x3cuy; 0xc5uy; 0x20uy; 0x1fuy; 0x1duy; 0x9euy; 0x5fuy; 0x3fuy;
          0x62uy; 0x23uy; 0x0euy; 0xb2uy; 0xcauy; 0xeauy; 0x01uy; 0x4buy; 0xecuy; 0xfbuy; 0xa6uy;
          0x0fuy; 0xcbuy; 0x1fuy; 0x39uy; 0x97uy; 0xaauy; 0x5buy; 0x3buy; 0xb6uy; 0x22uy; 0xb7uy;
          0x20uy; 0x5cuy; 0x71uy; 0x43uy; 0x48uy; 0xbauy; 0x15uy; 0x5cuy; 0x30uy; 0xa7uy; 0x9auy;
          0x2cuy; 0xeauy; 0x43uy; 0xb0uy; 0x70uy; 0xcauy; 0xdauy; 0x80uy; 0x7euy; 0x63uy; 0x0buy;
          0x40uy; 0x86uy; 0xb1uy; 0x29uy; 0x05uy; 0x18uy; 0x98uy; 0xe1uy; 0xd9uy; 0xe6uy; 0x8duy;
          0x1duy; 0x0euy; 0xccuy; 0x94uy; 0x29uy; 0xd2uy; 0x0duy; 0x6auy; 0x14uy; 0x03uy; 0xe0uy;
          0x03uy; 0x5auy; 0x44uy; 0x2buy; 0x37uy; 0xbfuy; 0x50uy; 0x8euy; 0xb8uy; 0x7euy; 0x8euy;
          0xa3uy; 0x47uy; 0xa3uy; 0xe6uy; 0x84uy; 0x27uy; 0xb6uy; 0xd4uy; 0x8euy; 0xd2uy; 0x99uy;
          0xbauy; 0x65uy; 0xecuy; 0xb3uy; 0x7buy; 0x38uy; 0x75uy; 0x4fuy; 0x45uy; 0x47uy; 0x42uy;
          0x3euy; 0xaeuy; 0xa2uy; 0xaeuy; 0xc4uy; 0x03uy; 0x33uy; 0x8duy; 0xb2uy; 0xdcuy; 0xfeuy;
          0x61uy; 0xcfuy; 0xf4uy; 0xa8uy; 0xd1uy; 0x7cuy; 0x38uy; 0x36uy; 0x56uy; 0x98uy; 0x1euy;
          0x18uy; 0x38uy; 0xa2uy; 0x38uy; 0x66uy; 0xb9uy; 0x1duy; 0x09uy; 0x69uy; 0x8fuy; 0x39uy;
          0x17uy; 0x5duy; 0x98uy; 0xafuy; 0x41uy; 0x75uy; 0xcauy; 0xeduy; 0x53uy
        ]
      in
      let cipher: list FStar.UInt8.t =
        [
          0xb2uy; 0x2buy; 0x87uy; 0xeauy; 0x30uy; 0xf4uy; 0x05uy; 0x09uy; 0x13uy; 0xf8uy; 0xf0uy;
          0x24uy; 0x1fuy; 0xc2uy; 0xaeuy; 0x2cuy; 0x31uy; 0x9fuy; 0x52uy; 0xe7uy
        ]
      in
      Vec SHA1 plain cipher)
  ]

let print_and_compare (str1:string) (str2:string) (len:Lib.IntTypes.size_nat) (test_expected:Lib.ByteSequence.lbytes len) (test_result:Lib.ByteSequence.lbytes len) =
  IO.print_string str1;
  List.iter (fun a -> IO.print_string (UInt8.to_string (Lib.RawIntTypes.u8_to_UInt8 a))) (Lib.Sequence.to_list test_expected);
  IO.print_string str2;
  List.iter (fun a -> IO.print_string (UInt8.to_string (Lib.RawIntTypes.u8_to_UInt8 a))) (Lib.Sequence.to_list test_result);
  Lib.ByteSequence.lbytes_eq test_expected test_result

let test_one (v: vec) =
  let Vec a plain tag = v in
  let expected = Seq.seq_of_list (List.Tot.map Lib.RawIntTypes.u8_from_UInt8 tag) in
  let computed = hash a (Seq.seq_of_list (List.Tot.map Lib.RawIntTypes.u8_from_UInt8 plain)) in
  print_and_compare "\nExpected: " "\nComputed: "(hash_length a) expected computed

let test () = List.for_all test_one test_vectors
